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

comparison OD.agda @ 314:6b09b5af9fcd

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 Fri, 03 Jul 2020 13:36:17 +0900
parents 8b5c8b685883
children 35e1214fa093
comparison
equal deleted inserted replaced
313:8b5c8b685883 314:6b09b5af9fcd
437 A ∩ t 437 A ∩ t
438 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩ 438 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
439 t 439 t
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 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)))
443 lemma9 = <-osuc 444 lemma9 = <-osuc
444 lemma8 : od→ord t o< od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))
445 lemma8 = {!!}
446 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) 445 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
447 lemma7 = ordtrans lemma8 (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 ) 446 lemma7 with osuc-≡< ( ⊆→o≤ t→A )
447 lemma7 | case1 eq = subst (λ k → k o< sup1 ) {!!} (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 )
448 lemma7 | case2 lt = ordtrans (subst₂ (λ j k → j o< k ) {!!} {!!} lt) (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 )
448 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) 449 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
449 lemma1 = subst (λ k → od→ord k 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))))
450 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) 451 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
451 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) 452 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
452 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 453 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where