# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593684355 -32400
# Node ID c1581ed5f38b5973811244c67946a931ea67d87d
# Parent  bf01e924e62e7f0c2d5a2f6d5cd993940a1a00a5
...

diff -r bf01e924e62e -r c1581ed5f38b OD.agda
--- a/OD.agda	Tue Jun 30 11:08:22 2020 +0900
+++ b/OD.agda	Thu Jul 02 19:05:55 2020 +0900
@@ -88,6 +88,7 @@
   od→ord : HOD  → Ordinal 
   ord→od : Ordinal  → HOD  
   c<→o<  :  {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y
+  ⊆→o≤  :   {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z)
   oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
   diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
   ==→o≡ : { x y : HOD  } → (od x == od y) → x ≡ y
@@ -218,16 +219,11 @@
      lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
      lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
 
-
-OPwr :  (A :  HOD ) → HOD 
-OPwr  A = Ord ( sup-o A ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )   
-
 record _⊆_ ( A B : HOD   ) : Set (suc n) where
   field 
      incl : { x : HOD } → A ∋ x →  B ∋ x
 
 open _⊆_
-
 infixr  220 _⊆_
 
 subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
@@ -236,6 +232,11 @@
     ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 
    } 
 
+power< : {A x : HOD  } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
+power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) diso (lemma y x∋y ) ) where
+    lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
+    lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y )
+
 open import Data.Unit
 
 ε-induction : { ψ : HOD  → Set (suc n)}
@@ -272,6 +273,10 @@
     Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  } ; odmax = {!!} ; <odmax = {!!} }
     _∈_ : ( A B : ZFSet  ) → Set n
     A ∈ B = B ∋ A
+
+    OPwr :  (A :  HOD ) → HOD 
+    OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )   
+
     Power : HOD  → HOD 
     Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
     -- ｛_｝ : ZFSet → ZFSet
@@ -393,9 +398,9 @@
               lemma1 :  {a : Ordinal } { t : HOD }
                  → (eq : ZFSubset (Ord a) t =h= t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
               lemma1  {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
-              lemma2 : def (od (Ord a)) (od→ord t)
-              lemma2 = {!!}
-              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
+              lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
+              lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t))) 
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
               lemma = sup-o< _ lemma2
 
          -- 
@@ -433,8 +438,9 @@
                  ≡⟨ sym (==→o≡ ( ∩-≡ 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))))
               lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
-              lemma7 = {!!}
+              lemma7 = ordtrans {!!} (sup-o< {!!} {!!}) 
               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 )