Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 315:35e1214fa093
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 03 Jul 2020 16:50:19 +0900 |
parents | 6b09b5af9fcd |
children | c030a9655e79 |
comparison
equal
deleted
inserted
replaced
314:6b09b5af9fcd | 315:35e1214fa093 |
---|---|
440 ∎ | 440 ∎ |
441 --- (od→ord t) o< (sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x)))) | 441 --- (od→ord t) o< (sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x)))) |
442 sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x))) | 442 sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x))) |
443 lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A))) | 443 lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A))) |
444 lemma9 = <-osuc | 444 lemma9 = <-osuc |
445 lemmab : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) )))) o< sup1 | |
446 lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 | |
447 lemmad : Ord (osuc (od→ord A)) ∋ t | |
448 lemmad = subst (λ k → k o< osuc (od→ord A)) {!!} {!!} -- ( ⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → {!!} ) ) | |
449 lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A) | |
450 lemmac = record { eq→ = {!!} ; eq← = {!!} } | |
451 lemmae : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A)) | |
452 lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac) | |
445 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) | 453 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) |
446 lemma7 with osuc-≡< ( ⊆→o≤ t→A ) | 454 lemma7 with osuc-≡< lemmad |
447 lemma7 | case1 eq = subst (λ k → k o< sup1 ) {!!} (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 ) | 455 lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab ) |
448 lemma7 | case2 lt = ordtrans (subst₂ (λ j k → j o< k ) {!!} {!!} lt) (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 ) | 456 lemma7 | case1 eq with osuc-≡< lemmad |
457 lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae {!!}) lemmab -- od→ord (Ord (od→ord A)) ≡ od→ord t | |
458 lemma7 | case1 eq | case2 lt = ordtrans {!!} (subst (λ k → k o< sup1) lemmae lemmab ) | |
449 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) | 459 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) |
450 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) | 460 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) |
451 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) | 461 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) |
452 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) | 462 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) |
453 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where | 463 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where |