Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 262:53744836020b
CH trying ...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 22 Sep 2019 20:26:32 +0900 |
parents | d9d178d1457c |
children | 2169d948159b |
comparison
equal
deleted
inserted
replaced
261:d9d178d1457c | 262:53744836020b |
---|---|
359 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) | 359 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) |
360 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) | 360 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) |
361 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) | 361 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) |
362 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy | 362 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy |
363 | 363 |
364 -- minimal-2 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) ) | |
365 -- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} ) | |
366 | |
364 OD→ZF : ZF | 367 OD→ZF : ZF |
365 OD→ZF = record { | 368 OD→ZF = record { |
366 ZFSet = OD | 369 ZFSet = OD |
367 ; _∋_ = _∋_ | 370 ; _∋_ = _∋_ |
368 ; _≈_ = _==_ | 371 ; _≈_ = _==_ |
545 lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t} ) | 548 lemma4 (sup-o< {λ x → od→ord (A ∩ ord→od x)} {od→ord t} ) |
546 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) | 549 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) |
547 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where | 550 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where |
548 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) | 551 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) |
549 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) | 552 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) |
553 | |
554 ord⊆power : (a : Ordinal) → (x : OD) → _⊆_ (Ord (osuc a)) (Power (Ord a)) {x} | |
555 ord⊆power a x lt = power← (Ord a) x lemma where | |
556 lemma : {y : OD} → x ∋ y → Ord a ∋ y | |
557 lemma y<x with osuc-≡< lt | |
558 lemma y<x | case1 refl = c<→o< y<x | |
559 lemma y<x | case2 x<a = ordtrans (c<→o< y<x) x<a | |
560 | |
561 -- continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_ (Power (Ord a)) (Ord (osuc a)) {x} | |
562 -- continuum-hyphotheis a x = ? | |
550 | 563 |
551 -- assuming axiom of choice | 564 -- assuming axiom of choice |
552 regularity : (x : OD) (not : ¬ (x == od∅)) → | 565 regularity : (x : OD) (not : ¬ (x == od∅)) → |
553 (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) | 566 (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) |
554 proj1 (regularity x not ) = x∋minimal x not | 567 proj1 (regularity x not ) = x∋minimal x not |