Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 314:6b09b5af9fcd
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 03 Jul 2020 13:36:17 +0900 |
| parents | 8b5c8b685883 |
| children | 35e1214fa093 |
line wrap: on
line diff
--- a/OD.agda Fri Jul 03 12:40:07 2020 +0900 +++ b/OD.agda Fri Jul 03 13:36:17 2020 +0900 @@ -439,12 +439,13 @@ t ∎ --- (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)))) + sup1 = sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x))) lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A))) lemma9 = <-osuc - lemma8 : od→ord t o< od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) - lemma8 = {!!} lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t) - lemma7 = ordtrans lemma8 (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 ) + lemma7 with osuc-≡< ( ⊆→o≤ t→A ) + lemma7 | case1 eq = subst (λ k → k o< sup1 ) {!!} (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 ) + lemma7 | case2 lt = ordtrans (subst₂ (λ j k → j o< k ) {!!} {!!} lt) (sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 ) lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x))) lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))) lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )