Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 152:996a67042f50
power set
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 09 Jul 2019 17:46:45 +0900 |
| parents | b5a337fb7a6d |
| children | f1801c4735d3 |
| files | HOD.agda |
| diffstat | 1 files changed, 26 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/HOD.agda Tue Jul 09 09:56:38 2019 +0900 +++ b/HOD.agda Tue Jul 09 17:46:45 2019 +0900 @@ -373,20 +373,20 @@ eq→ = λ {x} x<a → record { proj2 = x<a ; proj1 = def-subst {suc n} {_} {_} {b} {x} (inc (def-subst {suc n} {_} {_} {a} {_} x<a refl (sym diso) )) refl diso } ; eq← = λ {x} x<a∩b → proj2 x<a∩b } - ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → t ∋ x → Ord a ∋ x - ord-power→ a t P∋t {x} t∋x with osuc-≡< (sup-lb P∋t ) - ... | case1 eq = proj1 (def-subst t∋x (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl ) - ... | case2 lt = lemma3 where - sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))) - minsup : OD - minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) - Ltx : {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x - Ltx {n} {x} {t} lt = c<→o< lt - -- lemma1 hold because a subset of ordinals is ordinal - lemma1 : od→ord t o< od→ord minsup → minsup ∋ Ord (od→ord t) - lemma1 lt = {!!} - lemma3 : od→ord x o< a - lemma3 = otrans (proj1 (lemma1 lt)) (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) + -- ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → t ∋ x → Ord a ∋ x + -- ord-power→ a t P∋t {x} t∋x with osuc-≡< (sup-lb P∋t ) + -- ... | case1 eq = proj1 (def-subst t∋x (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl ) + -- ... | case2 lt = lemma3 where + -- sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))) + -- minsup : OD + -- minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) + -- Ltx : {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x + -- Ltx {n} {x} {t} lt = c<→o< lt + -- -- lemma1 hold because a subset of ordinals is ordinal + -- lemma1 : od→ord t o< od→ord minsup → minsup ∋ Ord (od→ord t) + -- lemma1 lt = {!!} + -- lemma3 : od→ord x o< a + -- lemma3 = otrans (proj1 (lemma1 lt)) (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) -- -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t -- Power A is a sup of ZFSubset A t, so Power A ∋ t @@ -428,13 +428,19 @@ lemma0 {x} t∋x = c<→o< (t→A t∋x) lemma3 : Def (Ord a) ∋ t lemma3 = ord-power← a t lemma0 - lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t)) - lemma4 = {!!} + lt1 : od→ord (A ∩ ord→od (od→ord t)) o< sup-o (λ x → od→ord (A ∩ ord→od x)) + lt1 = sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t} + lemma4 : (A ∩ ord→od (od→ord t)) ≡ t + lemma4 = let open ≡-Reasoning in begin + A ∩ ord→od (od→ord t) + ≡⟨ cong (λ k → A ∩ k) oiso ⟩ + A ∩ t + ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ + t + ∎ lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x)) - lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t} - ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where - lemma5 : od→ord (A ∩ Ord (od→ord t)) ≡ od→ord (A ∩ ord→od (od→ord t)) - lemma5 = cong (λ k → od→ord (A ∩ k )) {!!} + lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x))) + lemma4 (sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {od→ord t}) lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))