Members/kono/Proof/ZF-in-agda: OD.agda comparison

comparison OD.agda @ 317:57df07b63cae

Power done

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 03 Jul 2020 18:29:51 +0900
parents	c030a9655e79
children	9e0c97ab3a4a

comparison

equal deleted inserted replaced

-:c030a9655e79
+:57df07b63cae
 ;   ε-induction = ε-induction
 ;   infinity∅ = infinity∅
 ;   infinity = infinity
 ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
 ;   replacement← = replacement←
-;   replacement→ = replacement→
+;   replacement→ = λ {ψ} → replacement→ {ψ}
 -- ;   choice-func = choice-func
 -- ;   choice = choice
 } where
 pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )
 --
 power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x)
 power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
 a = od→ord A
 lemma2 : ¬ ( (y : HOD) → ¬ (t =h=  (A ∩ y)))
-lemma2 = replacement→ (OPwr (Ord (od→ord A))) t P∋t
+lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→ord A))) t P∋t
 lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x)
 lemma3 y eq not = not (proj1 (eq→ eq t∋x))
 lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ ord→od y)))
 lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 ))
 lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) →  ¬ ¬  (odef A (od→ord x))
 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 )) ⟩
+≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩
 t
 ∎
---- (od→ord t) o< (sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x))))
+sup1 : Ordinal
 sup1 =  sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x)))
 lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
 lemma9 = <-osuc
 lemmab : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
 lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9
 lemmad : Ord (osuc (od→ord A)) ∋ t
-lemmad = {!!}
+lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt)))
 lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A)
-lemmac = record { eq→ = {!!} ; eq← = {!!} }
+lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
+lemmaf : {x : Ordinal} → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
+lemmaf {x} lt = proj1 lt
+lemmag :  {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x
+lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt }
 lemmae : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
 lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac)
 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
 lemma7 with osuc-≡< lemmad
 lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
-lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → {!!} ))
+lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where
-lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae {!!}) lemmab -- od→ord (Ord (od→ord A)) ≡ od→ord t
+lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x
-lemma7 | case1 eq | case2 lt = ordtrans {!!} (subst (λ k → k o< sup1) lemmae lemmab )
+lemmah {x} lt = subst (λ k → def (od k) x ) (sym oiso) (subst (λ k → k o< (od→ord t))
+diso
+(c<→o< (subst₂ (λ j k → def (od j)  k) oiso (sym diso) lt )))
+lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where
+lemmai : od→ord (Ord (od→ord A)) ≡ od→ord t
+lemmai = let open ≡-Reasoning in begin
+od→ord (Ord (od→ord A))
+≡⟨ sym (cong (λ k → od→ord (Ord k)) eq) ⟩
+od→ord (Ord (od→ord t))
+≡⟨ sym diso ⟩
+od→ord (ord→od (od→ord (Ord (od→ord t))))
+≡⟨ sym eq1 ⟩
+od→ord (ord→od (od→ord t))
+≡⟨ diso ⟩
+od→ord t
+∎
+lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where
+lemmak : od→ord (ord→od (od→ord (Ord (od→ord t)))) ≡ od→ord (Ord (od→ord A))
+lemmak = let open ≡-Reasoning in begin
+od→ord (ord→od (od→ord (Ord (od→ord t))))
+≡⟨ diso ⟩
+od→ord (Ord (od→ord t))
+≡⟨ cong (λ k → od→ord (Ord k)) eq ⟩
+od→ord (Ord (od→ord A))
+∎
+lemmaj : od→ord t o< od→ord (Ord (od→ord A))
+lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt
 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
 lemma2 :  odef (in-codomain (OPwr (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))
-lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
+lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A  )))
 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a))
 ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
 lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y

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

comparison OD.agda @ 317:57df07b63cae