Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal.agda @ 264:fee0fab14de0
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 23 Sep 2019 10:43:48 +0900 |
parents | 2e75710a936b |
children | 30e419a2be24 |
comparison
equal
deleted
inserted
replaced
263:2e75710a936b | 264:fee0fab14de0 |
---|---|
248 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc | 248 ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc |
249 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc | 249 ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc |
250 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) | 250 ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) |
251 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) | 251 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) |
252 | 252 |
253 -- ZFSubset : (A x : OD ) → OD | |
254 -- ZFSubset A x = record { def = λ y → def A y ∧ def x y } | |
255 | |
256 -- Def : (A : OD ) → OD | |
257 -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) | |
258 | |
259 Ord-lemma : (a : Ordinal) (x : OD) → _⊆_ (ord→od a) (Ord a) {x} | |
260 Ord-lemma a x lt = o<-subst (c<→o< lt ) refl diso | |
261 | |
262 ⊆-trans : {a b c x : OD} → _⊆_ a b {x} → _⊆_ b c {x} → _⊆_ a c {x} | |
263 ⊆-trans a⊆b b⊆c a∋x = b⊆c (a⊆b a∋x) | |
264 | |
265 _∩_ = IsZF._∩_ isZF | |
266 | |
267 ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a) | |
268 ord-power-lemma {a} = record { eq→ = left ; eq← = right } where | |
269 left : {x : Ordinal} → def (Power (Ord a)) x → def (Def (Ord a)) x | |
270 left {x} lt = lemma1 where | |
271 lemma : od→ord ((Ord a) ∩ (ord→od x)) o< sup-o ( λ y → od→ord ((Ord a) ∩ (ord→od y))) | |
272 lemma = sup-o< { λ y → od→ord ((Ord a) ∩ (ord→od y))} {x} | |
273 lemma1 : x o< sup-o ( λ x → od→ord ( ZFSubset (Ord a) (ord→od x ))) | |
274 lemma1 = {!!} | |
275 right : {x : Ordinal } → def (Def (Ord a)) x → def (Power (Ord a)) x | |
276 right {x} lt = def-subst {_} {_} {Power (Ord a)} {x} (IsZF.power← isZF (Ord a) (ord→od x) {!!}) refl diso | |
277 | |
253 uncountable : (a y : Ordinal) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y) | 278 uncountable : (a y : Ordinal) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y) |
254 uncountable a y = TransFinite {n} {suc n} {λ z → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od z)} caseΦ caseOSuc y where | 279 uncountable a y = ⊆→o< lemma where |
255 caseΦ : (lx : Nat) → ((x : Ordinal) → x o< ordinal lx (Φ lx) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od x)) | 280 lemma-a : (x : OD ) → _⊆_ (ZFSubset (Ord a) (ord→od y)) (Ord a) {x} |
256 → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od (record { lv = lx ; ord = Φ lx })) | 281 lemma-a x lt = proj1 lt |
257 caseΦ lx prev = {!!} | 282 lemma : (x : OD ) → _⊆_ (Ord ( od→ord (ZFSubset (Ord a) (ord→od y)))) (Ord a) {x} |
258 caseOSuc : (lx : Nat) (ox : OrdinalD lx) | 283 lemma x = {!!} |
259 → ((y₁ : Ordinal) → y₁ o< ordinal lx (OSuc lx ox) → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y₁)) | |
260 → Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od (record { lv = lx ; ord = OSuc lx ox })) | |
261 caseOSuc lx ox prev = {!!} | |
262 | 284 |
263 continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} | 285 continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} |
264 continuum-hyphotheis a x = lemma2 where | 286 continuum-hyphotheis a x = lemma2 where |
265 lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a | 287 lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a |
266 lemma1 = {!!} | 288 lemma1 = {!!} |
267 lemma : _⊆_ (Def (Ord a)) (Ord (osuc a)) {x} | 289 lemma : _⊆_ (Def (Ord a)) (Ord (osuc a)) {x} |
268 lemma = o<→c< lemma1 | 290 lemma = o<→c< lemma1 |
269 lemma2 : _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} | 291 lemma2 : _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} |
270 lemma2 = {!!} | 292 lemma2 = subst ( λ k → _⊆_ k (Ord (osuc a)) {x} ) (sym (==→o≡ ord-power-lemma)) lemma |