# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558586907 -32400
# Node ID f10ceee99d00f41df942575eea45a53882bfddde
# Parent  4d64509067d03d1ed8fdc82d56eb951032c94d9e
¬ ( y c< x )  → x ≡ od∅

diff -r 4d64509067d0 -r f10ceee99d00 ordinal-definable.agda
--- a/ordinal-definable.agda	Thu May 23 02:32:02 2019 +0900
+++ b/ordinal-definable.agda	Thu May 23 13:48:27 2019 +0900
@@ -53,8 +53,8 @@
 ∅1 : {n : Level} →  ( x : OD {n} )  → ¬ ( x c< od∅ {n} )
 ∅1 {n} x (lift ())
 
-∅3 : {n : Level} →  ( x : Ordinal {n})  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
-∅3 {n} x = TransFinite {n} c1 c2 c3 x where
+∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
+∅3 {n} {x} = TransFinite {n} c1 c2 c3 x where
    c0 : Nat →  Ordinal {n}  → Set n
    c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x))  → x ≡ o∅ {n}
    c1 : ∀ (lx : Nat ) →  c0 lx (record { lv = Suc lx ; ord = ℵ lx } )  
@@ -77,6 +77,9 @@
    ... | t with t (case2 (s< (ℵΦ< {_} {_} {Φ (Suc lx)}))) 
    c3 .(Suc lx) (ℵ lx) d not | t | ()
 
+-- find : {n : Level} → ( x : Ordinal {n} ) → o∅ o< x → Ordinal {n}  
+-- exists : {n : Level} → ( x : Ordinal {n} ) → (0<x : o∅ o< x ) → find x 0<x o< x
+
 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
@@ -88,6 +91,67 @@
    lemma0 :  def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) →  def z (od→ord x)
    lemma0 dz  = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
 
+ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Ordinal {n}
+ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ())
+ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case2 ())
+ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case1 ())
+ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case2 Φ<) = record { lv = Zero ; ord = Φ 0 }
+ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case1 (s≤s x)) = record { lv = lv ; ord = Φ lv }
+ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case2 ())
+ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case1 (s≤s x)) = record { lv = (Suc lv) ; ord = ord }
+ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case2 ())
+ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case1 (s≤s z≤n)) = record { lv = lv ; ord = Φ lv }
+ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case2 ())
+
+∅4 : {n : Level} →  ( x : OD {n} )  →  x  ≡ od∅ {n}  → od→ord x ≡ o∅ {n}
+∅4 {n} x refl =  ∅3 lemma1 where
+  lemma0 :  (y : Ordinal {n}) → def ( od∅ {n} ) y →  ⊥
+  lemma0 y (lift ())
+  lemma1 : (y : Ordinal {n}) → y o< od→ord od∅ → ⊥
+  lemma1 y y<o = lemma0 y ( def-subst {n} {ord→od (od→ord od∅ )} {od→ord (ord→od y)} (o<→c< y<o) oiso diso )
+
+∅5 : {n : Level} →  ( x : Ordinal {n} )  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
+∅5 {n} record { lv = Zero ; ord = (Φ .0) } not = ⊥-elim (not refl) 
+∅5 {n} record { lv = Zero ; ord = (OSuc .0 ord) } not = case2 Φ<
+∅5 {n} record { lv = (Suc lv) ; ord = ord } not = case1 (s≤s z≤n)
+
+postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
+
+∅7 : {n : Level} →  { x : OD {n} } → ((z :  OD {n}) → ¬ ( z c< x ))  → x ≡ od∅
+∅7 {n} {x} not = cong ( λ k → record { def = k } ) lemma2 where
+   ⊥-eq :  ⊥ ≡ ⊥
+   ⊥-eq = refl
+   ⊥-leq : lift {_} {n} ⊥ ≡ lift {_} {n} ⊥
+   ⊥-leq = refl
+   lemma0 : Lift n ⊥ → ⊥
+   lemma0 (lift t ) = t
+   lemma0' :  ⊥ → Lift n ⊥
+   lemma0' t = lift t
+   lemma : (y : Ordinal {n}) → ¬ def x y
+   lemma y t = ⊥-elim ( not (ord→od y) (def-subst {n} {x} {y} t refl (sym diso) ) )
+   lemmak : (y : Ordinal {n}) → {m : Level}  → ¬ (Lift m (def x y ))
+   lemmak = {!!}
+   lemma1 : ( y : Ordinal {n}) → def x y ≡ def od∅ y 
+   lemma1 y with ⊥-leq 
+   lemma1 y | refl = {!!}
+   lemma2 : def x ≡ def od∅
+   lemma2 = extensionality ( λ y → lemma1 y )
+
+∅6 : {n : Level } ( x : Ordinal {suc n}) → o∅ o< x → ¬ x ≡ o∅
+∅6 {n} x lt eq with trio< {n} (o∅ {suc n}) x
+∅6 {n} x lt refl | tri< a ¬b ¬c = ¬b refl
+∅6 {n} x lt refl | tri≈ ¬a b ¬c =  ¬a lt
+∅6 {n} x lt refl | tri> ¬a ¬b c = ¬b refl
+
+∅2 : {n : Level} →  ( x : OD {n} )  → ¬ ( x  ≡ od∅ {n} ) → od∅ {n} c< x
+∅2 {n} x not with od→ord x
+... | ox = def-subst {n} {ord→od (od→ord x)} {od→ord (ord→od (o∅ {n}))}  (o<→c< (∅5 (od→ord x) lemma )) oiso lemma0 where
+   lemma0 : od→ord (ord→od (o∅ {n})) ≡ od→ord (od∅ {n})
+   lemma0 = trans diso (sym ( ∅4 (od∅ {n}) refl)  )
+   lemma : ¬ (od→ord x) ≡ o∅
+   lemma = {!!}
+
+
 open Ordinal
 
 HOD→ZF : {n : Level} → ZF {suc n} {suc n}
@@ -156,12 +220,10 @@
          union→ X x y (lift X∋x) (lift x∋y) = lift {!!}  where
             lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
             lemma {z} X∋z = {!!}
-         minimul : OD {n} → ( OD {n} ∧ OD {n} )
-         minimul x = record { proj1 = record { def = {!!} } ; proj2 = record { def = {!!} } }
-         regularity : (x : OD) → ¬ x ≡ od∅ →
-                Lift (suc n) (x ∋ proj1 (minimul x)) ∧
-                (Select (proj1 (minimul x ) , x) (λ x₁ → Lift (suc n) (proj1 ( minimul x ) ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)
-         proj1 ( regularity x non ) = lift lemma where
-            lemma : def x (od→ord (proj1 (minimul x)))
-            lemma = {!!}
+         minimul : (x : OD {n} ) → ¬ x ≡ od∅ → OD {n} 
+         minimul record { def = def } not = {!!}
+         regularity : (x : OD) → (not : ¬ x ≡ od∅ ) →
+                Lift (suc n) (x ∋ minimul x not ) ∧
+                (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)
+         proj1 ( regularity x non ) = {!!}
          proj2 ( regularity x non ) = {!!}
diff -r 4d64509067d0 -r f10ceee99d00 zf.agda
--- a/zf.agda	Thu May 23 02:32:02 2019 +0900
+++ b/zf.agda	Thu May 23 13:48:27 2019 +0900
@@ -71,8 +71,8 @@
      -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extentionality :  ( A B z  : ZFSet  ) → (( A ∋ z ) ⇔ (B ∋ z) ) → A ≈ B
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
-     minimul : ZFSet → ( ZFSet ∧ ZFSet )
-     regularity : ∀( x : ZFSet  ) → ¬ (x ≈ ∅) → ( proj1 ( minimul x ) ∈ x ∧  ( proj1 ( minimul x )  ∩ x  ≈ ∅ ) )
+     minimul : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 
+     regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimul x not  ∈ x ∧  (  minimul x not  ∩ x  ≈ ∅ ) )
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ Select X (  λ y → x ≈ y )) ∈ infinite