# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593768591 -32400
# Node ID 57df07b63cae4a6771768da168655196da2c9149
# Parent  c030a9655e79df04f0153c58985187b147bb286a
Power done

diff -r c030a9655e79 -r 57df07b63cae OD.agda
--- a/OD.agda	Fri Jul 03 16:51:44 2020 +0900
+++ b/OD.agda	Fri Jul 03 18:29:51 2020 +0900
@@ -311,7 +311,7 @@
        ;   infinity = infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement← = replacement←
-       ;   replacement→ = replacement→
+       ;   replacement→ = λ {ψ} → replacement→ {ψ}
        -- ;   choice-func = choice-func
        -- ;   choice = choice
      } where
@@ -415,7 +415,7 @@
          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)))
@@ -435,34 +435,64 @@
                     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 | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae {!!}) lemmab -- od→ord (Ord (od→ord A)) ≡ od→ord t
-              lemma7 | case1 eq | case2 lt = ordtrans {!!} (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 → lemmah lt )) where
+                  lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x
+                  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))