Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison LEMC.agda @ 331:12071f79f3cf
HOD done
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 05 Jul 2020 16:56:21 +0900 |
parents | 0faa7120e4b5 |
children | 2a8a51375e49 |
comparison
equal
deleted
inserted
replaced
330:0faa7120e4b5 | 331:12071f79f3cf |
---|---|
110 p : HOD | 110 p : HOD |
111 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where | 111 p = record { od = record { def = λ y1 → odef x y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where |
112 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) | 112 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u) |
113 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) | 113 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt)) |
114 np : ¬ (p =h= od∅) | 114 np : ¬ (p =h= od∅) |
115 np p∅ = NP (λ y p∋y → ∅< p∋y p∅ ) | 115 np p∅ = NP (λ y p∋y → ∅< {p} {_} p∋y p∅ ) |
116 y1choice : choiced p | 116 y1choice : choiced p |
117 y1choice = choice-func p np | 117 y1choice = choice-func p np |
118 y1 : HOD | 118 y1 : HOD |
119 y1 = a-choice y1choice | 119 y1 = a-choice y1choice |
120 y1prop : (x ∋ y1) ∧ (u ∋ y1) | 120 y1prop : (x ∋ y1) ∧ (u ∋ y1) |
124 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u | 124 Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u |
125 Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) | 125 Min2 x u u∋x = (ε-induction1 {λ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u } induction x u u∋x ) |
126 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced x | 126 cx : {x : HOD} → ¬ (x =h= od∅ ) → choiced x |
127 cx {x} nx = choice-func x nx | 127 cx {x} nx = choice-func x nx |
128 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD | 128 minimal : (x : HOD ) → ¬ (x =h= od∅ ) → HOD |
129 minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) | 129 minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) |
130 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) | 130 x∋minimal : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) ) |
131 x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) | 131 x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) |
132 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) | 132 minimal-1 : (x : HOD ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord y) ) |
133 minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y | 133 minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y |
134 | 134 |
135 | 135 |
136 | 136 |