# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1561912045 -32400
# Node ID 1114081eb51f24948c59e60c94a9bfe71e647971
# Parent  20e59a28d263a4e2eaa795d37d90f57a37949209
power set

diff -r 20e59a28d263 -r 1114081eb51f HOD.agda
--- a/HOD.agda	Mon Jul 01 00:20:56 2019 +0900
+++ b/HOD.agda	Mon Jul 01 01:27:25 2019 +0900
@@ -346,13 +346,13 @@
          --    In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity
          --
          power→ : (A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x = proj1 lemma-s where
+         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 = otrans A (proj1 (lemma lt )) (c<→o< {suc n} {x} {t} t∋x) where
               minsup :  HOD
-              minsup =  ZFSubset A ( Ord ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
-              lemma-s : ZFSubset A ( Ord ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
-              lemma-s with osuc-≡<  (sup-lb  P∋t)  
-              lemma-s | case1 eq = proj1 ( def-subst t∋x ()  ? )
-              lemma-s | case2 lt = {!!} 
+              minsup =  ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 
+              lemma : od→ord t o< od→ord minsup → minsup ∋ t
+              lemma lt = {!!}
          -- 
          -- 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
@@ -363,7 +363,8 @@
               lemma-eq :  ZFSubset A t == t
               eq→ lemma-eq {z} w = proj2 w 
               eq← lemma-eq {z} w = record { proj2 = w  ;
-                 proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
+                 proj1 = def-subst {suc n} {_} {_} {A} {z}
+                    ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
               lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
               lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ lemma-eq ))
               lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))