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

comparison src/zorn.agda @ 987:c8c60a05b39b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
is-max?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 13 Nov 2022 10:23:50 +0900
parents 557f8145d3c1
children 9a85233384f7
comparison
equal deleted inserted replaced
986:557f8145d3c1 987:c8c60a05b39b
1431 ss<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ c<A)) 1431 ss<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ c<A))
1432 ... | case2 sc<sa = sc<sa 1432 ... | case2 sc<sa = sc<sa
1433 ... | case1 sc=sa = ⊥-elim ( nmx record { maximal = * d ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm spd) 1433 ... | case1 sc=sa = ⊥-elim ( nmx record { maximal = * d ; as = subst (λ k → odef A k) (sym &iso) (MinSUP.asm spd)
1434 ; ¬maximal<x = λ {x} ax → subst₂ (λ j k → ¬ ( j < k)) refl *iso (zc10 sc=sa ax) } ) where 1434 ; ¬maximal<x = λ {x} ax → subst₂ (λ j k → ¬ ( j < k)) refl *iso (zc10 sc=sa ax) } ) where
1435 zc10 : supf c ≡ supf (& A) → {x : Ordinal } → odef A x → ¬ ( d << x ) 1435 zc10 : supf c ≡ supf (& A) → {x : Ordinal } → odef A x → ¬ ( d << x )
1436 zc10 = ? -- supf x o≤ supf c → supf x ≡ supf c ∨ supf x o< supf c 1436 zc10 = ? where
1437 zc11 : {z : Ordinal } → odef (ZChain.chain zc) z → supf z o< supf (& A)
1438 zc11 = ?
1439 sc≤c : c o≤ supf c
1440 sc≤c = MinSUP.minsup msp1 ? ?
1441 sc=c : supf c ≡ c
1442 sc=c = ?
1443 d≤c : c o≤ d
1444 d≤c = MinSUP.minsup msp1 ? ?
1445 -- supf x o≤ supf c → supf x ≡ supf c ∨ supf x o< supf c
1437 -- c << x → x is sup of chain or x = f ( .. ( f c )) 1446 -- c << x → x is sup of chain or x = f ( .. ( f c ))
1438 -- c << x → x is not in chain 1447 -- c o≤ x (by minimulity)
1439 -- supf c o≤ x (minimulity) 1448 -- odef chain z → supf z o< supf (& A) ≡ supf c → supf c is sup of chain, by minimulity c o≤ supf c
1440 -- odef chain z → supf z o< supf (& A) ≡ supf c → minimulity c o≤ supf c
1441 -- supf c o≤ supf (supf c) o≤ supf x o≤ supf (& A) 1449 -- supf c o≤ supf (supf c) o≤ supf x o≤ supf (& A)
1442 -- supf c ≡ supf (supf c) ≡ supf x ≡ supf (& A) means supf of FClosure of (supf c) is Maximal 1450 -- supf c ≡ supf (supf c) ≡ supf x ≡ supf (& A) means supf of FClosure of (supf c) is Maximal
1443 1451
1444 zorn00 : Maximal A 1452 zorn00 : Maximal A
1445 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM 1453 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM