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

comparison OD.agda @ 313:8b5c8b685883

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 12:40:07 +0900
parents c1581ed5f38b
children 6b09b5af9fcd
comparison
equal deleted inserted replaced
312:c1581ed5f38b 313:8b5c8b685883
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 lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
443 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 = {!!}
442 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) 446 lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
443 lemma7 = ordtrans {!!} (sup-o< {!!} {!!}) 447 lemma7 = ordtrans lemma8 (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 )
444 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) 448 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
445 lemma1 = subst (λ k → od→ord k 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))))
446 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 ) 450 lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
447 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t) 451 lemma2 : odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
448 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where 452 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where