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

comparison src/zorn.agda @ 760:0dc7999b1d50

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 25 Jul 2022 06:41:40 +0900
parents 944f50265914
children 9307f895891c
comparison
equal deleted inserted replaced
759:944f50265914 760:0dc7999b1d50
366 Zorn-lemma {A} 0<A supP = zorn00 where 366 Zorn-lemma {A} 0<A supP = zorn00 where
367 <-irr0 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥ 367 <-irr0 : {a b : HOD} → A ∋ a → A ∋ b → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
368 <-irr0 {a} {b} A∋a A∋b = <-irr 368 <-irr0 {a} {b} A∋a A∋b = <-irr
369 z07 : {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A 369 z07 : {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
370 z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) 370 z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
371 z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
372 z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
371 s : HOD 373 s : HOD
372 s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 374 s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A ))
373 as : A ∋ * ( & s ) 375 as : A ∋ * ( & s )
374 as = subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ) 376 as = subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) )
375 as0 : odef A (& s ) 377 as0 : odef A (& s )
471 m03 with proj2 ua 473 m03 with proj2 ua
472 ... | ch-init fc = ⟪ proj1 ua , ch-init fc ⟫ 474 ... | ch-init fc = ⟪ proj1 ua , ch-init fc ⟫
473 ... | ch-is-sup u u≤x is-sup fc with trio< u px 475 ... | ch-is-sup u u≤x is-sup fc with trio< u px
474 ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup fc ⟫ -- u o< osuc x 476 ... | tri< a ¬b ¬c = ⟪ proj1 ua , ch-is-sup u (o<→≤ a) is-sup fc ⟫ -- u o< osuc x
475 ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup fc ⟫ 477 ... | tri≈ ¬a u=px ¬c = ⟪ proj1 ua , ch-is-sup u (o≤-refl0 u=px) is-sup fc ⟫
476 ... | tri> ¬a ¬b c = ? -- u = x 478 ... | tri> ¬a ¬b c = ? -- u = x → u = sup → (b o< x → b < a ) → ⊥
477 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b 479 m04 : odef (UnionCF A f mf ay (ZChain.supf zc) px) b
478 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab 480 m04 = ZChain1.is-max (prev px px<x) m03 b<px ab
479 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl lt) } ) a<b 481 (case2 record {x<sup = λ {z} lt → IsSup.x<sup is-sup (chain-mono2 x ( o<→≤ (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc )) o≤-refl lt) } ) a<b
480 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) ? (subst (λ k → FClosure A f k b) ? (init ab)) ⟫ -- b = px case, u = px u< osuc x 482 ... | tri≈ ¬a b=px ¬c = ⟪ ab , ch-is-sup b (o<→≤ b<x) m06 (subst (λ k → FClosure A f k b) m05 (init ab)) ⟫ where
483 m06 : ChainP A f mf ay (ZChain.supf zc) b b
484 m06 = ?
485 m05 : b ≡ ZChain.supf zc b
486 m05 = sym ( ZChain.sup=u zc {b} {ab} (z09 ab)
487 record { x<sup = λ {z} uz → IsSup.x<sup is-sup (chain-mono2 x (osucc b<x) o≤-refl uz ) } )
488 -- b = px case, u = px u< osuc x
481 ... | no lim = record { is-max = is-max } where 489 ... | no lim = record { is-max = is-max } where
482 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a → 490 is-max : {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
483 b o< x → (ab : odef A b) → 491 b o< x → (ab : odef A b) →
484 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab → 492 HasPrev A (UnionCF A f mf ay (ZChain.supf zc) x) ab f ∨ IsSup A (UnionCF A f mf ay (ZChain.supf zc) x) ab →
485 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b 493 * a < * b → odef (UnionCF A f mf ay (ZChain.supf zc) x) b