Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 344:e0916a632971

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
possible order restriction makes ω ZFSet
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 Jul 2020 14:45:57 +0900
parents 34e71402d579
children f895642a8460
files OD.agda
diffstat 1 files changed, 7 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Jul 13 14:30:37 2020 +0900
+++ b/OD.agda	Mon Jul 13 14:45:57 2020 +0900
@@ -106,7 +106,7 @@
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
 
--- possible restriction
+-- possible order restriction
 hod-ord< :  {x : HOD } → Set n
 hod-ord< {x} =  od→ord x o< next (odmax x)
 
@@ -237,6 +237,12 @@
        lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
        lemmab1 = ho<
 
+pair<y : {x y : HOD } → y ∋ x  → od→ord (x , x) o< osuc (od→ord y)
+pair<y {x} {y} y∋x = ⊆→o≤ lemma where
+   lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
+   lemma (case1 refl) = y∋x
+   lemma (case2 refl) = y∋x
+
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
@@ -259,12 +265,6 @@
 od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
 
 -- if we have od→ord (x , x) ≡ osuc (od→ord x),  ⊆→o≤ → c<→o<
-pair<y : {x y : HOD } → y ∋ x  → od→ord (x , x) o< osuc (od→ord y)
-pair<y {x} {y} y∋x = ⊆→o≤ lemma where
-   lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
-   lemma (case1 refl) = y∋x
-   lemma (case2 refl) = y∋x
-
 ⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
    →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) )
    →   {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y 
@@ -394,14 +394,6 @@
         lemma (isuc {y} x) = lemma2 where
             lemma0 : y o< next o∅
             lemma0 = lemma x
-            lemma3 : odef (u y ) y 
-            lemma3 = FExists _ (λ {z} t not → not (od→ord (ord→od y , ord→od y)) record { proj1 = case2 refl ; proj2 = lemma4 }) (λ not → not y (infinite-d y)) where
-                lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y 
-                lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl)
-            lemma5 : y o< odmax (u y)
-            lemma5 = <odmax (u y) lemma3
-            lemma6 : y o< odmax (ord→od y , (ord→od y , ord→od y))
-            lemma6 = <odmax (ord→od y , (ord→od y , ord→od y)) (subst ( λ k → def (od (ord→od y , (ord→od y , ord→od y))) k ) diso (case1 refl))
             lemma8 : od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
             lemma8 = ho<
             ---           (x,y) < next (omax x y) < next (osuc y) = next y 
@@ -409,8 +401,6 @@
             lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
             lemma81 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
             lemma81 = nexto=n (subst (λ k →  od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
-            lemma91 : od→ord (ord→od y) o< od→ord (ord→od y , ord→od y)
-            lemma91 = c<→o< (case1 refl) 
             lemma9 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
             lemma9 = lemmaa (c<→o< (case1 refl))
             lemma71 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))