Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 157:afc030b7c8d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explict logical definition of Union failed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Jul 2019 08:04:16 +0900
parents 3e7475fb28db
children b97b4ee06f01
files HOD.agda
diffstat 1 files changed, 6 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Thu Jul 11 20:00:30 2019 +0900
+++ b/HOD.agda	Sun Jul 14 08:04:16 2019 +0900
@@ -339,8 +339,13 @@
          union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
          union-u {X} {z} U>z = ord→od ( osuc ( od→ord z ) )
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
-         union→ X z u xx = {!!}
+         union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
+              ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
 
+         union-u' : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
+         union-u' {X} {z} U>z = record { def = λ x → ¬ ( (u : Ordinal ) → ¬ (def X u) ∧ (ord→od u ∋ z ) ∧ ( u ≡ x ) ) }
+         union←' :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+         union←' X z UX∋z =  TransFiniteExists {suc (suc n)} {λ x → {!!} } {!!} {!!} where
          union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
          union← X z UX∋z = record { proj1 = lemma ; proj2 = lemma2 } where
              lemma : X ∋ union-u {X} {z} UX∋z