Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/BAlgbra.agda @ 1096:55ab5de1ae02
recovery
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 23 Dec 2022 12:54:05 +0900 |
parents | 6c22ee73ff06 |
children | 256a3ba634f6 |
comparison
equal
deleted
inserted
replaced
1095:08b6aa6870d9 | 1096:55ab5de1ae02 |
---|---|
56 [a-b]∩b=0 : { A B : HOD } → (A \ B) ∩ B ≡ od∅ | 56 [a-b]∩b=0 : { A B : HOD } → (A \ B) ∩ B ≡ od∅ |
57 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) | 57 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) |
58 ; eq→ = λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) } | 58 ; eq→ = λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) } |
59 | 59 |
60 U-F=∅→F⊆U : {F U : HOD} → ((x : Ordinal) → ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U | 60 U-F=∅→F⊆U : {F U : HOD} → ((x : Ordinal) → ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U |
61 U-F=∅→F⊆U {F} {U} not = record { incl = gt02 } where | 61 U-F=∅→F⊆U {F} {U} not = gt02 where |
62 gt02 : { x : Ordinal } → odef F x → odef U x | 62 gt02 : { x : Ordinal } → odef F x → odef U x |
63 gt02 {x} fx with ODC.∋-p O U (* x) | 63 gt02 {x} fx with ODC.∋-p O U (* x) |
64 ... | yes y = subst (λ k → odef U k ) &iso y | 64 ... | yes y = subst (λ k → odef U k ) &iso y |
65 ... | no n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ ) | 65 ... | no n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ ) |
66 | 66 |
67 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) | 67 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) |
68 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | 68 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
69 lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x | 69 lemma1 : {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x |
70 lemma1 {x} lt = lemma3 lt where | 70 lemma1 {x} record { owner = owner ; ao = abo ; ox = ox } with pair=∨ (subst₂ (λ j k → odef (j , k ) owner) (sym *iso) (sym *iso) abo ) |
71 lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (* y) x → ¬ (¬ ( odef A x ∨ odef B x) ) | 71 ... | case1 a=o = case1 (subst (λ k → odef k x ) ( begin |
72 lemma4 {y} z with proj1 z | 72 * owner ≡⟨ cong (*) (sym a=o) ⟩ |
73 lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) *iso (proj2 z)) ) | 73 * (& A) ≡⟨ *iso ⟩ |
74 lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) *iso (proj2 z)) ) | 74 A ∎ ) ox ) where open ≡-Reasoning |
75 lemma3 : (((u : Ordinal ) → ¬ odef (A , B) u ∧ odef (* u) x) → ⊥) → odef (A ∪ B) x | 75 ... | case2 b=o = case2 (subst (λ k → odef k x ) (trans (cong (*) (sym b=o)) *iso ) ox) |
76 lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not) -- choice | |
77 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x | 76 lemma2 : {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x |
78 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A | 77 lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) A |
79 ⟪ case1 refl , d→∋ A A∋x ⟫ ) | 78 ⟪ case1 refl , d→∋ A A∋x ⟫ ) |
80 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B | 79 lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) &iso ( IsZF.union→ isZF (A , B) (* x) B |
81 ⟪ case2 refl , d→∋ B B∋x ⟫ ) | 80 ⟪ case2 refl , d→∋ B B∋x ⟫ ) |