# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1569203028 -32400
# Node ID fee0fab14de032d304eb2c92185bd2372738c86c
# Parent  2e75710a936bd4f05eb7258a112551c7675c3a3e
...

diff -r 2e75710a936b -r fee0fab14de0 ordinal.agda
--- a/ordinal.agda	Mon Sep 23 09:16:39 2019 +0900
+++ b/ordinal.agda	Mon Sep 23 10:43:48 2019 +0900
@@ -250,15 +250,37 @@
   ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl )
   ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
 
+  -- ZFSubset : (A x : OD  ) → OD 
+  -- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
+
+  -- Def :  (A :  OD ) → OD 
+  -- Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
+
+  Ord-lemma : (a : Ordinal) (x : OD) → _⊆_ (ord→od a) (Ord a) {x}
+  Ord-lemma a x lt = o<-subst (c<→o< lt ) refl diso
+
+  ⊆-trans :  {a b c x : OD}  →  _⊆_ a b {x}  →   _⊆_ b c {x}  →   _⊆_ a c {x}    
+  ⊆-trans a⊆b b⊆c a∋x  = b⊆c (a⊆b a∋x)
+
+  _∩_ = IsZF._∩_ isZF
+
+  ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a)
+  ord-power-lemma {a} = record { eq→ = left ; eq← = right } where
+       left : {x : Ordinal} → def (Power (Ord a)) x → def (Def (Ord a)) x
+       left {x} lt = lemma1 where
+          lemma : od→ord ((Ord a) ∩ (ord→od x)) o< sup-o ( λ y → od→ord ((Ord a) ∩ (ord→od y)))
+          lemma = sup-o< { λ y → od→ord ((Ord a) ∩ (ord→od y))} {x} 
+          lemma1 : x o<  sup-o  ( λ x → od→ord ( ZFSubset (Ord a) (ord→od x ))) 
+          lemma1 = {!!}
+       right : {x : Ordinal } → def (Def (Ord a)) x → def (Power (Ord a)) x
+       right {x} lt = def-subst {_} {_} {Power (Ord a)} {x} (IsZF.power← isZF (Ord a) (ord→od x) {!!}) refl diso
+
   uncountable : (a y : Ordinal) →  Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y) 
-  uncountable a y = TransFinite {n} {suc n} {λ z → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od z)} caseΦ caseOSuc y where
-       caseΦ : (lx : Nat) → ((x : Ordinal) → x o< ordinal lx (Φ lx) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od x))
-             → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od (record { lv = lx ; ord = Φ lx }))
-       caseΦ lx prev = {!!}
-       caseOSuc : (lx : Nat) (ox : OrdinalD lx)
-             → ((y₁ : Ordinal) → y₁ o< ordinal lx (OSuc lx ox) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y₁))
-             → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od (record { lv = lx ; ord = OSuc lx ox }))
-       caseOSuc lx ox prev = {!!}
+  uncountable a y = ⊆→o<  lemma  where
+       lemma-a :  (x : OD ) → _⊆_ (ZFSubset (Ord a) (ord→od y)) (Ord a) {x}
+       lemma-a x lt = proj1 lt
+       lemma :  (x : OD ) → _⊆_ (Ord ( od→ord (ZFSubset (Ord a) (ord→od y)))) (Ord a) {x}
+       lemma x = {!!}
 
   continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
   continuum-hyphotheis a x = lemma2 where
@@ -267,4 +289,4 @@
        lemma : _⊆_ (Def (Ord a))  (Ord (osuc a)) {x}
        lemma = o<→c< lemma1
        lemma2 : _⊆_ (Power (Ord a))  (Ord (osuc a)) {x}
-       lemma2 = {!!}
+       lemma2 = subst ( λ k → _⊆_ k (Ord (osuc a)) {x} ) (sym (==→o≡ ord-power-lemma)) lemma