Members/kono/Proof/ZF-in-agda: src/zorn.agda comparison

comparison src/zorn.agda @ 1088:125605b5bf47

supf-idem is not so easy

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sun, 18 Dec 2022 16:56:17 +0900
parents	2fa98e3c0fa3
children

comparison

equal deleted inserted replaced

-:2fa98e3c0fa3
+:125605b5bf47
 record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  ( z : Ordinal ) : Set (Level.suc n) where
 field
 supf :  Ordinal → Ordinal
+cfcs  : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
+order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b
 asupf :  {x : Ordinal } → odef A (supf x)
 supf-mono : {x y : Ordinal } → x o≤  y → supf x o≤ supf y
 zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x
 is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
-cfcs  : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
-supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
 chain : HOD
 chain = UnionCF A f ay supf z
 chain⊆A : chain ⊆' A
 chain⊆A = λ lt → proj1 lt
 ... | case2 lt = case2 (subst₂ (λ j k → j << k ) &iso (sym (supf-is-minsup u≤z )) lt )
 initial : {x : Ordinal } → x o≤ z → odef (UnionCF A f ay supf x) x →  y ≤ x
 initial {x} x≤z ⟪ aa , ch-init fc ⟫ = s≤fc y f mf fc
 initial {x} x≤z ⟪ aa , ch-is-sup u u<x is-sup fc ⟫ = ≤-ftrans (fcy<sup (ordtrans u<x x≤z) (init ay refl)) (s≤fc _ f mf fc)
-supfeq : {a b : Ordinal } → a o≤ z →  b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b
-supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b)
-... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
-IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
-... | tri≈ ¬a b ¬c = b
-... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
-IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
-union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b
-union-max {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
-z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w
-z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
-z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
-u<b : u o< b
-u<b = ordtrans u<a (supf-inject sa<sb )
-z48 : {w : Ordinal } → odef (UnionCF A f ay supf b ) w → odef ( UnionCF A f ay supf a ) w
-z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
-z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
-u<a : u o< a
-u<a = supf-inject ( osucprev (begin
-osuc (supf u)  ≡⟨ cong osuc su=u ⟩
-osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
-z  ≤⟨ z≤sa ⟩
-supf a ∎ )) where open o≤-Reasoning O
-sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
-→ IsSUP A (UnionCF A f ay supf b) b  → supf b ≡ b
-sup=u {b} ab b≤z is-sup = z50 where
-z48 : supf b o≤ b
-z48 = IsMinSUP.minsup (is-minsup b≤z) ab (λ ux → IsSUP.x≤sup is-sup ux )
-z50 : supf b ≡ b
-z50 with trio< (supf b) b
-... | tri< sb<b ¬b ¬c = ⊥-elim ( o≤> z47 sb<b ) where
-z47 : b o≤ supf b
-z47 = zo≤sz b≤z
-... | tri≈ ¬a b ¬c = b
-... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb )
-x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x
-x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x
-... | case2 le = le
-... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where
-z46 : odef (UnionCF A f ay supf x) (f (supf x))
-z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf  z47 )) ⟫ where
-z47 : supf (supf x) ≡ supf x
-z47 = supf-idem x≤z  sx≤z
-z45 : f (supf x) ≤ supf x
-z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46
-order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b
-order {a} {b} {w} b≤z sa<sb fc with  x<y∨y≤x (supf a) z
-... | case2 z≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where
-z27 : supf a ≡ supf b
-z27 = supfeq (OrdTrans (o<→≤ (supf-inject sa<sb)) b≤z) b≤z ( union-max z≤sa b≤z sa<sb)
-... | case1 sa<z = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where
-sa<b : supf a o< b
-sa<b with x<y∨y≤x (supf a) b
-... | case1 lt = lt
-... | case2 b≤sa = ⊥-elim ( o≤> b≤sa ( supf-inject ( osucprev ( begin
-osuc (supf (supf a))  ≡⟨ cong osuc (supf-idem (ordtrans (supf-inject sa<sb) b≤z) (o<→≤ sa<z))  ⟩
-osuc (supf a)  ≤⟨ osucc sa<sb ⟩
-supf b ∎ )))) where open o≤-Reasoning O
-supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b
-supf-mono< {a} {b} b≤z sa<sb  with order {a} {b} b≤z sa<sb (init asupf refl)
-... | case2 lt = lt
-... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb )
 f-total : IsTotalOrderSet chain
 f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ =
 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where
 fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
 b<a = subst₂ (λ j k → j < k ) *iso *iso lt
 ft00 :   Tri ( a <  b) ( a ≡  b) ( b <  a )
 ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca))
 f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ =
 subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso  (fcn-cmp y f mf fca fcb )
+supf-mono< : {a b : Ordinal } → b o≤ z → supf a o< supf b → supf a << supf b
+supf-mono< {a} {b} b≤z sa<sb  with order {a} {b} b≤z sa<sb (init asupf refl)
+... | case2 lt = lt
+... | case1 eq = ⊥-elim ( o<¬≡ eq sa<sb )
+supfeq : {a b : Ordinal } → a o≤ z →  b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b
+supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b)
+... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
+IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
+IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
+union-max : {a b : Ordinal } → z o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b
+union-max {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
+z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w
+z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
+u<b : u o< b
+u<b = ordtrans u<a (supf-inject sa<sb )
+z48 : {w : Ordinal } → odef (UnionCF A f ay supf b ) w → odef ( UnionCF A f ay supf a ) w
+z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
+u<a : u o< a
+u<a = supf-inject ( osucprev (begin
+osuc (supf u)  ≡⟨ cong osuc su=u ⟩
+osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
+z  ≤⟨ z≤sa ⟩
+supf a ∎ )) where open o≤-Reasoning O
+sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
+→ IsSUP A (UnionCF A f ay supf b) b  → supf b ≡ b
+sup=u {b} ab b≤z is-sup = z50 where
+z48 : supf b o≤ b
+z48 = IsMinSUP.minsup (is-minsup b≤z) ab (λ ux → IsSUP.x≤sup is-sup ux )
+z50 : supf b ≡ b
+z50 with trio< (supf b) b
+... | tri< sb<b ¬b ¬c = ⊥-elim ( o≤> z47 sb<b ) where
+z47 : b o≤ supf b
+z47 = zo≤sz b≤z
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb )
+supf-idem : {b : Ordinal } → b o≤ z → supf b o≤ z  → supf (supf b) ≡ supf b
+supf-idem {b} b≤z sfb≤x = z52 where
+z54 :  {w : Ordinal} → odef (UnionCF A f ay supf (supf b)) w → (w ≡ supf b) ∨ (w << supf b)
+z54 {w} ⟪ aw , ch-init fc ⟫ = fcy<sup b≤z fc
+z54 {w} ⟪ aw , ch-is-sup u u<x su=u fc ⟫ = order b≤z (subst (λ k → k o< supf b) (sym su=u) u<x)  fc where
+u<b : u o< b
+u<b = supf-inject (subst (λ k → k o< supf b ) (sym (su=u)) u<x )
+z52 : supf (supf b) ≡ supf b
+z52 = sup=u asupf sfb≤x  record { ax = asupf  ; x≤sup = z54  }
+x≤supfx : {x : Ordinal } → x o≤ z → supf x o≤ z → x o≤ supf x
+x≤supfx {x} x≤z sx≤z with x<y∨y≤x (supf x) x
+... | case2 le = le
+... | case1 spx<px = ⊥-elim ( <<-irr z45 (proj1 ( mf< (supf x) asupf ))) where
+z46 : odef (UnionCF A f ay supf x) (f (supf x))
+z46 = ⟪ proj2 ( mf (supf x) asupf ) , ch-is-sup (supf x) spx<px z47 (fsuc _ (init asupf  z47 )) ⟫ where
+z47 : supf (supf x) ≡ supf x
+z47 = supf-idem x≤z  sx≤z
+z45 : f (supf x) ≤ supf x
+z45 = IsMinSUP.x≤sup (is-minsup x≤z ) z46
+-- order may proved is-minsup and supf-idem, but supf-idem uses order
+--    Is proving supf-idem is easier than order?
+--
+order0 : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b
+order0 {a} {b} {w} b≤z sa<sb fc with  x<y∨y≤x (supf a) z
+... | case2 z≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where
+z27 : supf a ≡ supf b
+z27 = supfeq (OrdTrans (o<→≤ (supf-inject sa<sb)) b≤z) b≤z ( union-max z≤sa b≤z sa<sb)
+... | case1 sa<z = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where
+sa<b : supf a o< b
+sa<b with x<y∨y≤x (supf a) b
+... | case1 lt = lt
+... | case2 b≤sa = ⊥-elim ( o≤> b≤sa ( supf-inject ( osucprev ( begin
+osuc (supf (supf a))  ≡⟨ cong osuc (supf-idem (ordtrans (supf-inject sa<sb) b≤z) (o<→≤ sa<z))  ⟩
+osuc (supf a)  ≤⟨ osucc sa<sb ⟩
+supf b ∎ )))) where open o≤-Reasoning O
 record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf< : <-monotonic-f A f)
 {y : Ordinal} (ay : odef A y)  (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
 supf = ZChain.supf zc
 field
 z25 {w} ⟪ ua , ch-is-sup u u<x su=u fc  ⟫ = sup ⟪ ua , ch-is-sup u u<x
 (trans (sf1=sf0 u≤px)  su=u)  (fcpu fc u≤px)  ⟫ where
 u≤px : u o≤ px
 u≤px = ordtrans u<x z≤px
+supfeq1 : {a b : Ordinal } → a o≤ x →  b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b
+supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b)
+... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
+IsMinSUP.minsup (is-minsup b≤z) asupf1 (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
+IsMinSUP.minsup (is-minsup a≤z) asupf1 (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
+union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b
+union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
+z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w
+z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
+u<b : u o< b
+u<b = ordtrans u<a (supf-inject0 supf1-mono sa<sb )
+z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w
+z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
+u<a : u o< a
+u<a = supf-inject0 supf1-mono ( osucprev (begin
+osuc (supf1 u)  ≡⟨ cong osuc su=u ⟩
+osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
+x  ≤⟨ z≤sa ⟩
+supf1 a ∎ )) where open o≤-Reasoning O
 zo≤sz : {z : Ordinal} →  z o≤ x → z o≤ supf1 z
 zo≤sz {z} z≤x with osuc-≡< z≤x
 ... | case2 z<x = subst (λ k → z o≤ k) (sym (sf1=sf0 (zc-b<x _ z<x ))) (ZChain.zo≤sz zc (zc-b<x _ z<x ))
 ... | case1 refl with osuc-≡< (supf1-mono (o<→≤ (px<x))) --   px o≤ supf1 px o≤ supf1 x ≡ sp1 → x o≤ sp1
 ... | case2 lt = begin
 sp1 ∎ where open ≡-Reasoning
 zc40 :  f (supf0 px) ≤ supf0 px
 zc40 = subst (λ k → f (supf0 px) ≤ k ) (sym zc39)
 ( MinSUP.x≤sup sup1 (case2 ⟪ fsuc _ (init (ZChain.asupf zc) refl) , subst (λ k → k o< x) (sym zc37) px<x ⟫  ))
+order : {a b : Ordinal} {w : Ordinal} →
+b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
+order {a} {b} {w} b≤x sa<sb fc = z20 where
+a<b : a o< b
+a<b = supf-inject0 supf1-mono sa<sb
+a≤px : a o≤ px
+a≤px with trio< a px
+... | tri< a ¬b ¬c = o<→≤ a
+... | tri≈ ¬a b ¬c = o≤-refl0 b
+... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → a o< k) (sym (Oprev.oprev=x op))
+( ordtrans<-≤ a<b b≤x) ⟫ ) -- px o< a o< b o≤ x
+z20 : w ≤ supf1 b
+z20 with trio< b px
+... | tri< b<px ¬b ¬c = ZChain.order zc (o<→≤ b<px) (subst (λ k → k o< supf0 b) (sf1=sf0 (o<→≤ (ordtrans a<b b<px))) sa<sb)
+(fcup fc (o<→≤ (ordtrans a<b b<px)))
+... | tri≈ ¬a b=px ¬c = IsMinSUP.x≤sup (ZChain.is-minsup zc (o≤-refl0 b=px)) z26  where
+a≤x : a o≤ x
+a≤x = o<→≤ (ordtrans ( subst (λ k → a o< k ) b=px a<b ) px<x )
+z26 : odef ( UnionCF A f ay supf0 b ) w
+z26 with x<y∨y≤x (supf1 a) b
+... | case2 b≤sa = z27 where
+z27 : odef (UnionCF A f ay supf0 b) w
+z27 with osuc-≡< b≤sa
+... | case2 b<sa = ⊥-elim ( o<¬≡ ( supfeq1 a≤x b≤x
+( union-max1 x≤sa b≤x (subst (λ k → supf1 a o< k) (sym (sf1=sf0 (o≤-refl0 b=px)))  sa<sb) ))
+(ordtrans<-≤ sa<sb (o≤-refl0 (sym (sf1=sf0 (o≤-refl0 b=px))) ))) where
+x≤sa : x o≤ supf1 a
+x≤sa = subst (λ k → k o≤ supf1 a ) (trans (cong osuc b=px) (Oprev.oprev=x op)) (osucc b<sa )
+... | case1 b=sa = ⊥-elim (o<¬≡ sa=sb sa<sb)  where
+sa=sb : supf1 a ≡ supf0 b
+sa=sb = begin
+supf1 a ≡⟨ sf1=sf0 a≤px ⟩
+supf0 a ≡⟨ sym (ZChain.supf-idem zc a≤px (o≤-refl0 (sym (trans (sym b=px) (trans b=sa (sf1=sf0 a≤px) )))))  ⟩
+supf0 (supf0 a) ≡⟨ cong supf0 (sym (sf1=sf0 a≤px )) ⟩
+supf0 (supf1 a) ≡⟨ cong supf0 (sym b=sa) ⟩
+supf0 b ∎ where open ≡-Reasoning
+... | case1 sa<b with cfcs a<b b≤x sa<b fc
+... | ⟪ ua , ch-init fc ⟫ = ⟪ ua , ch-init fc ⟫
+... | ⟪ ua , ch-is-sup u u<x su=u fc ⟫ = ⟪ ua , ch-is-sup u u<x (trans (sym (sf1=sf0 u≤px)) su=u) (fcup fc u≤px)  ⟫ where
+u≤px : u o≤ px
+u≤px = o<→≤ ( subst (λ k → u o< k ) b=px u<x )
+... | tri> ¬a ¬b px<b with x<y∨y≤x (supf1 a) b
+... | case1 sa<b = MinSUP.x≤sup sup1 (zc11 ( chain-mono f mf ay supf1 supf1-mono b≤x (cfcs a<b b≤x sa<b fc)))
+... | case2 b≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where -- x=b  x o≤ sa   UnionCF a ≡ UnionCF b → supf1 a ≡ supfb b → ⊥
+b=x : b ≡ x
+b=x with trio< b x
+... | tri< a ¬b ¬c = ⊥-elim ( ¬p<x<op ⟪ px<b , zc-b<x _ a ⟫   ) -- px o< b o< x
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b c = ⊥-elim ( o≤> b≤x c ) -- x o< b ≤ x
+a≤x : a o≤ x
+a≤x = o<→≤ ( subst (λ k → a o< k ) b=x a<b )
+sf1b=sp1 : supf1 b ≡ sp1
+sf1b=sp1  = sf1=sp1 (subst (λ k → px o< k) (trans (Oprev.oprev=x op) (sym b=x))  <-osuc)
+z27 : supf1 a ≡ sp1
+z27 = trans ( supfeq1 a≤x b≤x ( union-max1 (subst (λ k → k o≤ supf1 a) b=x b≤sa)
+b≤x (subst (λ k → supf1 a o< k ) (sym sf1b=sp1)  sa<sb )  ) ) sf1b=sp1
 ... | no lim with trio< x o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay)
-; supf-mono = λ _ → o≤-refl
+; supf-mono = λ _ → o≤-refl ; order = λ _ s<s → ⊥-elim ( o<¬≡ refl s<s )
 ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0)))    } where
 mf : ≤-monotonic-f A f
 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
 mf00 : * x < * (f x)
 mf00 = proj1 ( mf< x ax )
 ym = MinSUP.sup (ysup f mf ay)
 zo≤sz : {z : Ordinal} → z o≤ x → z o≤ MinSUP.sup (ysup f mf ay)
 zo≤sz {z} z≤x with osuc-≡< z≤x
 ... | case1 refl = subst (λ k → k o≤ _) (sym x=0) o∅≤z
 ... | case2 lt = ⊥-elim ( ¬x<0  (subst (λ k → z o< k ) x=0 lt ) )
 is-minsup : {z : Ordinal} → z o≤ x →
 IsMinSUP A (UnionCF A f ay (λ _ → MinSUP.sup (ysup f mf ay)) z) (MinSUP.sup (ysup f mf ay))
 is-minsup {z} z≤x with osuc-≡< z≤x
 → ym o≤ s
 is01 {s} as sup = MinSUP.minsup (ysup f mf ay) as is02 where
 is02 : {w : Ordinal } →  odef (uchain f mf ay) w → (w ≡ s) ∨ (w << s)
 is02 fc = sup ⟪ A∋fc _ f mf fc , ch-init fc ⟫
 ... | case2 lt = ⊥-elim ( ¬x<0  (subst (λ k → z o< k ) x=0 lt ) )
 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = order
 ; zo≤sz = zo≤sz   ; is-minsup = is-minsup ; cfcs = cfcs    }  where
 mf : ≤-monotonic-f A f
 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where
 mf00 : * x < * (f x)
 z50 = o≤-refl0 z49
 z48 : odef pchainU (f spu)
 z48 = ⟪  proj2 (mf _ (MinSUP.as usup) ) , ic-isup _ (subst (λ k → k o< x) refl spu<x) z50
 (fsuc _ (init (ZChain.asupf (pzc (ob<x lim spu<x))) z49)) ⟫
+supfeq1 : {a b : Ordinal } → a o≤ x →  b o≤ x → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b → supf1 a ≡ supf1 b
+supfeq1 {a} {b} a≤z b≤z ua=ub with trio< (supf1 a) (supf1 b)
+... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
+IsMinSUP.minsup (is-minsup b≤z) asupf (λ {z} uzb → IsMinSUP.x≤sup (is-minsup a≤z) (subst (λ k → odef k z) (sym ua=ub) uzb)) ) sa<sb )
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
+IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
+union-max1 : {a b : Ordinal } → x o≤ supf1 a → b o≤ x → supf1 a o< supf1 b → UnionCF A f ay supf1 a ≡ UnionCF A f ay supf1 b
+union-max1 {a} {b} z≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
+z47 : {w : Ordinal } → odef (UnionCF A f ay supf1 a ) w → odef ( UnionCF A f ay supf1 b ) w
+z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where
+u<b : u o< b
+u<b = ordtrans u<a (supf-inject0 supf-mono sa<sb )
+z48 : {w : Ordinal } → odef (UnionCF A f ay supf1 b ) w → odef ( UnionCF A f ay supf1 a ) w
+z48 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫
+z48 {w} ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = ⟪ aw , ch-is-sup u u<a su=u fc ⟫ where
+u<a : u o< a
+u<a = supf-inject0 supf-mono ( osucprev (begin
+osuc (supf1 u)  ≡⟨ cong osuc su=u ⟩
+osuc u  ≤⟨ osucc (ordtrans<-≤ u<b b≤z ) ⟩
+x  ≤⟨ z≤sa ⟩
+supf1 a ∎ )) where open o≤-Reasoning O
+order : {a b w : Ordinal } → b o≤ x → supf1 a o< supf1 b → FClosure A f (supf1 a) w → w ≤ supf1 b
+order {a} {b} {w} b≤x sa<sb fc with osuc-≡< b≤x
+... | case2 b<x = subst (λ k → w ≤ k ) (sym (trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl ))))  (
+ZChain.order (pzc b<x) o≤-refl
+(subst₂ (λ j k → j o< k ) (trans (sf1=sf a<x) (zeq _ _ (osucc a<b) (o<→≤ <-osuc)))
+(trans (sf1=sf b<x) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl)))  sa<sb)
+(subst  (λ k → FClosure A f k w) (trans (sf1=sf a<x) (zeq _ _ (osucc a<b) (o<→≤ <-osuc)) )  fc ) ) where
+a<b : a o< b
+a<b = supf-inject0 supf-mono sa<sb
+a<x : a o< x
+a<x = ordtrans<-≤ a<b b≤x
+... | case1 refl = subst (λ k → w ≤ k ) (sym (sf1=spu refl)) (  zc40 (subst₂ (λ j k → j o< k) (sf1=sf a<x) (sf1=spu refl) sa<sb)
+(subst (λ k → FClosure A f k w) (sf1=sf a<x) fc )) where
+a<x : a o< x
+a<x = supf-inject0 supf-mono sa<sb
+zc40 : ZChain.supf (pzc  (ob<x lim a<x )) a o< spu → FClosure A f (ZChain.supf (pzc  (ob<x lim a<x )) a) w → w ≤ spu
+zc40 sa<sp fc with x<y∨y≤x (supfz a<x) x
+... | case1 sa<x = z29 where
+z28 : odef (UnionCF A f ay supf1 b) w
+z28 = cfcs a<x o≤-refl (subst (λ k → k o< x) (sym (sf1=sf a<x)) sa<x) (subst (λ k → FClosure A f k w ) (sym (sf1=sf a<x)) fc )
+z29 : w ≤ spu
+z29 with z28
+... | ⟪ aw , ch-init fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-init fc ⟫
+... | ⟪ aw , ch-is-sup u u<b su=u fc ⟫ = MinSUP.x≤sup usup ⟪ aw , ic-isup u u<b z30
+(subst (λ k → FClosure A f k w) (sf1=sf u<b) fc) ⟫ where
+z30 : supfz u<b o≤ u
+z30 = o≤-refl0 ( trans (sym (sf1=sf u<b)) su=u )
+... | case2 x≤sa = ⊥-elim ( o<¬≡ z27 sa<sb ) where
+z27 : supf1 a ≡ supf1 b
+z27 = begin
+supf1 a  ≡⟨ ( supfeq1 (o<→≤ a<x) o≤-refl ( union-max1 (subst (λ k → x o≤ k ) (sym (sf1=sf a<x)) x≤sa ) b≤x sa<sb) ) ⟩
+supf1 x  ∎ where open ≡-Reasoning
 ---
 --- the maximum chain  has fix point of any ≤-monotonic function
 ---
 SZ : ( f : Ordinal → Ordinal ) → (mf< : <-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf< ay x

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

comparison src/zorn.agda @ 1088:125605b5bf47