Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/BAlgbra.agda @ 480:6c22ee73ff06
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 03 Apr 2022 17:53:13 +0900 |
parents | 31f0a5a745a5 |
children | 55ab5de1ae02 |
comparison
equal
deleted
inserted
replaced
479:fea0c2454b85 | 480:6c22ee73ff06 |
---|---|
54 ¬∅∋ {x} = ¬x<0 | 54 ¬∅∋ {x} = ¬x<0 |
55 | 55 |
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 | |
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 | |
62 gt02 : { x : Ordinal } → odef F x → odef U x | |
63 gt02 {x} fx with ODC.∋-p O U (* x) | |
64 ... | yes y = subst (λ k → odef U k ) &iso y | |
65 ... | no n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ ) | |
59 | 66 |
60 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) | 67 ∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B ) |
61 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | 68 ∪-Union {A} {B} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
62 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 |
63 lemma1 {x} lt = lemma3 lt where | 70 lemma1 {x} lt = lemma3 lt where |