Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 396:8c092c042093
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 27 Jul 2020 15:11:54 +0900 |
parents | 19687f3304c9 |
children | 44a484f17f26 |
comparison
equal
deleted
inserted
replaced
395:77c6123f49ee | 396:8c092c042093 |
---|---|
43 ... | no ¬p = ⊥-elim ( notnot ¬p ) | 43 ... | no ¬p = ⊥-elim ( notnot ¬p ) |
44 | 44 |
45 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A | 45 power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A |
46 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where | 46 power→⊆ A t PA∋t = record { incl = λ {x} t∋x → double-neg-eilm (λ not → t1 t∋x (λ x → not x) ) } where |
47 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) | 47 t1 : {x : HOD } → t ∋ x → ¬ ¬ (A ∋ x) |
48 t1 = zf.IsZF.power→ isZF A t PA∋t | 48 t1 = power→ A t PA∋t |
49 | 49 |
50 --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice | 50 --- With assuption of HOD is ordered, p ∨ ( ¬ p ) <=> axiom of choice |
51 --- | 51 --- |
52 record choiced ( X : Ordinal ) : Set n where | 52 record choiced ( X : Ordinal ) : Set n where |
53 field | 53 field |
108 ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo p } ) | 108 ... | yes p = case2 ( record { a-choice = x ; is-in = ∋oo p } ) |
109 ... | no ¬p = lemma where | 109 ... | no ¬p = lemma where |
110 lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (od→ord X) | 110 lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced (od→ord X) |
111 lemma1 y with ∋-p X (ord→od y) | 111 lemma1 y with ∋-p X (ord→od y) |
112 lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } ) | 112 lemma1 y | yes y<X = case2 ( record { a-choice = y ; is-in = ∋oo y<X } ) |
113 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) ) | 113 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (d→∋ X y<X) ) |
114 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (od→ord X) | 114 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced (od→ord X) |
115 lemma = ∀-imply-or lemma1 | 115 lemma = ∀-imply-or lemma1 |
116 have_to_find : choiced (od→ord X) | 116 have_to_find : choiced (od→ord X) |
117 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where | 117 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where |
118 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥) | 118 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥) |
146 p : HOD | 146 p : HOD |
147 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where | 147 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where |
148 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) | 148 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) |
149 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) | 149 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) |
150 np : ¬ (p =h= od∅) | 150 np : ¬ (p =h= od∅) |
151 np p∅ = NP (λ y p∋y → ∅< {p} {_} (subst (λ k → odef p k) (sym diso) p∋y) p∅ ) | 151 np p∅ = NP (λ y p∋y → ∅< {p} {_} (d→∋ p p∋y) p∅ ) |
152 y1choice : choiced (od→ord p) | 152 y1choice : choiced (od→ord p) |
153 y1choice = choice-func p np | 153 y1choice = choice-func p np |
154 y1 : HOD | 154 y1 : HOD |
155 y1 = ord→od (a-choice y1choice) | 155 y1 = ord→od (a-choice y1choice) |
156 y1prop : (x ∋ y1) ∧ (u ∋ y1) | 156 y1prop : (x ∋ y1) ∧ (u ∋ y1) |