Home | Metamath
Proof Explorer Theorem List (p. 103 of 462) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29004) |
Hilbert Space Explorer
(29005-30527) |
Users' Mathboxes
(30528-46188) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | alephreg 10201 | A successor aleph is regular. Theorem 11.15 of [TakeutiZaring] p. 103. (Contributed by Mario Carneiro, 9-Mar-2013.) |
⊢ (cf‘(ℵ‘suc 𝐴)) = (ℵ‘suc 𝐴) | ||
Theorem | pwcfsdom 10202* | A corollary of Konig's Theorem konigth 10188. Theorem 11.28 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.) |
⊢ 𝐻 = (𝑦 ∈ (cf‘(ℵ‘𝐴)) ↦ (har‘(𝑓‘𝑦))) ⇒ ⊢ (ℵ‘𝐴) ≺ ((ℵ‘𝐴) ↑m (cf‘(ℵ‘𝐴))) | ||
Theorem | cfpwsdom 10203 | A corollary of Konig's Theorem konigth 10188. Theorem 11.29 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (2o ≼ 𝐵 → (ℵ‘𝐴) ≺ (cf‘(card‘(𝐵 ↑m (ℵ‘𝐴))))) | ||
Theorem | alephom 10204 | From canth2 8804, we know that (ℵ‘0) < (2↑ω), but we cannot prove that (2↑ω) = (ℵ‘1) (this is the Continuum Hypothesis), nor can we prove that it is less than any bound whatsoever (i.e. the statement (ℵ‘𝐴) < (2↑ω) is consistent for any ordinal 𝐴). However, we can prove that (2↑ω) is not equal to (ℵ‘ω), nor (ℵ‘(ℵ‘ω)), on cofinality grounds, because by Konig's Theorem konigth 10188 (in the form of cfpwsdom 10203), (2↑ω) has uncountable cofinality, which eliminates limit alephs like (ℵ‘ω). (The first limit aleph that is not eliminated is (ℵ‘(ℵ‘1)), which has cofinality (ℵ‘1).) (Contributed by Mario Carneiro, 21-Mar-2013.) |
⊢ (card‘(2o ↑m ω)) ≠ (ℵ‘ω) | ||
Theorem | smobeth 10205 | The beth function is strictly monotone. This function is not strictly the beth function, but rather bethA is the same as (card‘(𝑅1‘(ω +o 𝐴))), since conventionally we start counting at the first infinite level, and ignore the finite levels. (Contributed by Mario Carneiro, 6-Jun-2013.) (Revised by Mario Carneiro, 2-Jun-2015.) |
⊢ Smo (card ∘ 𝑅1) | ||
Theorem | nd1 10206 | A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑦 ∈ 𝑧) | ||
Theorem | nd2 10207 | A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑧 ∈ 𝑦) | ||
Theorem | nd3 10208 | A lemma for proving conditionless ZFC axioms. (Contributed by NM, 2-Jan-2002.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑧 𝑥 ∈ 𝑦) | ||
Theorem | nd4 10209 | A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑧 𝑦 ∈ 𝑥) | ||
Theorem | axextnd 10210 | A version of the Axiom of Extensionality with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 14-Aug-2003.) (New usage is discouraged.) |
⊢ ∃𝑥((𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧) | ||
Theorem | axrepndlem1 10211* | Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) | ||
Theorem | axrepndlem2 10212 | Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (New usage is discouraged.) |
⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(𝑧 ∈ 𝑥 ↔ ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))) | ||
Theorem | axrepnd 10213 | A version of the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(∀𝑦 𝑧 ∈ 𝑥 ↔ ∃𝑥(∀𝑧 𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑))) | ||
Theorem | axunndlem1 10214* | Lemma for the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axunnd 10215 | A version of the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥) | ||
Theorem | axpowndlem1 10216 | Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) | ||
Theorem | axpowndlem2 10217* | Lemma for the Axiom of Power Sets with no distinct variable conditions. Revised to remove a redundant antecedent from the consequence. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (Revised and shortened by Wolf Lammen, 9-Jun-2019.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))) | ||
Theorem | axpowndlem3 10218* | Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 4-Jan-2002.) (Revised by Mario Carneiro, 10-Dec-2016.) (Proof shortened by Wolf Lammen, 10-Jun-2019.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) | ||
Theorem | axpowndlem4 10219 | Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) (New usage is discouraged.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) | ||
Theorem | axpownd 10220 | A version of the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 4-Jan-2002.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) | ||
Theorem | axregndlem1 10221 | Lemma for the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))) | ||
Theorem | axregndlem2 10222* | Lemma for the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
Theorem | axregnd 10223 | A version of the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Wolf Lammen, 18-Aug-2019.) (New usage is discouraged.) |
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
Theorem | axinfndlem1 10224* | Lemma for the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.) |
⊢ (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) | ||
Theorem | axinfnd 10225 | A version of the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.) |
⊢ ∃𝑥(𝑦 ∈ 𝑧 → (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) | ||
Theorem | axacndlem1 10226 | Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) | ||
Theorem | axacndlem2 10227 | Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) | ||
Theorem | axacndlem3 10228 | Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.) |
⊢ (∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) | ||
Theorem | axacndlem4 10229* | Lemma for the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) |
⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) | ||
Theorem | axacndlem5 10230* | Lemma for the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) |
⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) | ||
Theorem | axacnd 10231 | A version of the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) |
⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) | ||
Theorem | zfcndext 10232* | Axiom of Extensionality ax-ext 2708, reproved from conditionless ZFC version and predicate calculus. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) | ||
Theorem | zfcndrep 10233* | Axiom of Replacement ax-rep 5184, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) | ||
Theorem | zfcndun 10234* | Axiom of Union ax-un 7528, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfcndpow 10235* | Axiom of Power Sets ax-pow 5263, reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness" dtru 5268. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfcndreg 10236* | Axiom of Regularity ax-reg 9213, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) | ||
Theorem | zfcndinf 10237* | Axiom of Infinity ax-inf 9258, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5267 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) | ||
Theorem | zfcndac 10238* | Axiom of Choice ax-ac 10078, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) | ||
Syntax | cgch 10239 | Extend class notation to include the collection of sets that satisfy the GCH. |
class GCH | ||
Definition | df-gch 10240* | Define the collection of "GCH-sets", or sets for which the generalized continuum hypothesis holds. In this language the generalized continuum hypothesis can be expressed as GCH = V. A set 𝑥 satisfies the generalized continuum hypothesis if it is finite or there is no set 𝑦 strictly between 𝑥 and its powerset in cardinality. The continuum hypothesis is equivalent to ω ∈ GCH. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ GCH = (Fin ∪ {𝑥 ∣ ∀𝑦 ¬ (𝑥 ≺ 𝑦 ∧ 𝑦 ≺ 𝒫 𝑥)}) | ||
Theorem | elgch 10241* | Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ GCH ↔ (𝐴 ∈ Fin ∨ ∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)))) | ||
Theorem | fingch 10242 | A finite set is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ Fin ⊆ GCH | ||
Theorem | gchi 10243 | The only GCH-sets which have other sets between it and its power set are finite sets. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 ∈ GCH ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴) → 𝐴 ∈ Fin) | ||
Theorem | gchen1 10244 | If 𝐴 ≤ 𝐵 < 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐴 = 𝐵 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴)) → 𝐴 ≈ 𝐵) | ||
Theorem | gchen2 10245 | If 𝐴 < 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → 𝐵 ≈ 𝒫 𝐴) | ||
Theorem | gchor 10246 | If 𝐴 ≤ 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then either 𝐴 = 𝐵 or 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → (𝐴 ≈ 𝐵 ∨ 𝐵 ≈ 𝒫 𝐴)) | ||
Theorem | engch 10247 | The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ GCH ↔ 𝐵 ∈ GCH)) | ||
Theorem | gchdomtri 10248 | Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac 10300. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 ∈ GCH ∧ (𝐴 ⊔ 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) | ||
Theorem | fpwwe2cbv 10249* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 3-Jun-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} ⇒ ⊢ 𝑊 = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} | ||
Theorem | fpwwe2lem1 10250* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} ⇒ ⊢ 𝑊 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) | ||
Theorem | fpwwe2lem2 10251* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))) | ||
Theorem | fpwwe2lem3 10252* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋𝑊𝑅) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → ((◡𝑅 “ {𝐵})𝐹(𝑅 ∩ ((◡𝑅 “ {𝐵}) × (◡𝑅 “ {𝐵})))) = 𝐵) | ||
Theorem | fpwwe2lem4 10253* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴) | ||
Theorem | fpwwe2lem5 10254* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) & ⊢ 𝑀 = OrdIso(𝑅, 𝑋) & ⊢ 𝑁 = OrdIso(𝑆, 𝑌) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑁) & ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (◡𝑀‘𝐶) = (◡𝑁‘𝐶))) | ||
Theorem | fpwwe2lem6 10255* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) & ⊢ 𝑀 = OrdIso(𝑅, 𝑋) & ⊢ 𝑁 = OrdIso(𝑆, 𝑌) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑁) & ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶𝑆(𝑁‘𝐵) ∧ (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷)))) | ||
Theorem | fpwwe2lem7 10256* | Lemma for fpwwe2 10262. Show by induction that the two isometries 𝑀 and 𝑁 agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) & ⊢ 𝑀 = OrdIso(𝑅, 𝑋) & ⊢ 𝑁 = OrdIso(𝑆, 𝑌) & ⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) ⇒ ⊢ (𝜑 → 𝑀 = (𝑁 ↾ dom 𝑀)) | ||
Theorem | fpwwe2lem8 10257* | Lemma for fpwwe2 10262. Given two well-orders 〈𝑋, 𝑅〉 and 〈𝑌, 𝑆〉 of parts of 𝐴, one is an initial segment of the other. (The 𝑂 ⊆ 𝑃 hypothesis is in order to break the symmetry of 𝑋 and 𝑌.) (Contributed by Mario Carneiro, 15-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) & ⊢ 𝑀 = OrdIso(𝑅, 𝑋) & ⊢ 𝑁 = OrdIso(𝑆, 𝑌) & ⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) ⇒ ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∧ 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))) | ||
Theorem | fpwwe2lem9 10258* | Lemma for fpwwe2 10262. Given two well-orders 〈𝑋, 𝑅〉 and 〈𝑌, 𝑆〉 of parts of 𝐴, one is an initial segment of the other. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) ⇒ ⊢ (𝜑 → ((𝑋 ⊆ 𝑌 ∧ 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) ∨ (𝑌 ⊆ 𝑋 ∧ 𝑆 = (𝑅 ∩ (𝑋 × 𝑌))))) | ||
Theorem | fpwwe2lem10 10259* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋)) | ||
Theorem | fpwwe2lem11 10260* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 18-May-2015.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → 𝑋 ∈ dom 𝑊) | ||
Theorem | fpwwe2lem12 10261* | Lemma for fpwwe2 10262. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) | ||
Theorem | fpwwe2 10262* | Given any function 𝐹 from well-orderings of subsets of 𝐴 to 𝐴, there is a unique well-ordered subset 〈𝑋, (𝑊‘𝑋)〉 which "agrees" with 𝐹 in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 9649. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)))) | ||
Theorem | fpwwecbv 10263* | Lemma for fpwwe 10265. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} ⇒ ⊢ 𝑊 = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧))} | ||
Theorem | fpwwelem 10264* | Lemma for fpwwe 10265. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝐹‘(◡𝑅 “ {𝑦})) = 𝑦)))) | ||
Theorem | fpwwe 10265* | Given any function 𝐹 from the powerset of 𝐴 to 𝐴, canth2 8804 gives that the function is not injective, but we can say rather more than that. There is a unique well-ordered subset 〈𝑋, (𝑊‘𝑋)〉 which "agrees" with 𝐹 in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 9649. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝐹‘𝑌) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)))) | ||
Theorem | canth4 10266* | An "effective" form of Cantor's theorem canth 7172. For any function 𝐹 from the powerset of 𝐴 to 𝐴, there are two definable sets 𝐵 and 𝐶 which witness non-injectivity of 𝐹. Corollary 1.3 of [KanamoriPincus] p. 416. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} & ⊢ 𝐵 = ∪ dom 𝑊 & ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐷⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝐷) → (𝐵 ⊆ 𝐴 ∧ 𝐶 ⊊ 𝐵 ∧ (𝐹‘𝐵) = (𝐹‘𝐶))) | ||
Theorem | canthnumlem 10267* | Lemma for canthnum 10268. (Contributed by Mario Carneiro, 19-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} & ⊢ 𝐵 = ∪ dom 𝑊 & ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ⇒ ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) | ||
Theorem | canthnum 10268 | The set of well-orderable subsets of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 8804. Corollary 1.4(a) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 19-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ (𝒫 𝐴 ∩ dom card)) | ||
Theorem | canthwelem 10269* | Lemma for canthwe 10270. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ 𝑂 = {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} & ⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ 𝐵 = ∪ dom 𝑊 & ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ⇒ ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:𝑂–1-1→𝐴) | ||
Theorem | canthwe 10270* | The set of well-orders of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 8804. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ 𝑂 = {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ 𝑂) | ||
Theorem | canthp1lem1 10271 | Lemma for canthp1 10273. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴) | ||
Theorem | canthp1lem2 10272* | Lemma for canthp1 10273. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝜑 → 1o ≺ 𝐴) & ⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o)) & ⊢ (𝜑 → 𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})–1-1-onto→𝐴) & ⊢ 𝐻 = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) & ⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐻‘(◡𝑟 “ {𝑦})) = 𝑦))} & ⊢ 𝐵 = ∪ dom 𝑊 ⇒ ⊢ ¬ 𝜑 | ||
Theorem | canthp1 10273 | A slightly stronger form of Cantor's theorem: For 1 < 𝑛, 𝑛 + 1 < 2↑𝑛. Corollary 1.6 of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (1o ≺ 𝐴 → (𝐴 ⊔ 1o) ≺ 𝒫 𝐴) | ||
Theorem | finngch 10274 | The exclusion of finite sets from consideration in df-gch 10240 is necessary, because otherwise finite sets larger than a singleton would violate the GCH property. (Contributed by Mario Carneiro, 10-Jun-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 1o ≺ 𝐴) → (𝐴 ≺ (𝐴 ⊔ 1o) ∧ (𝐴 ⊔ 1o) ≺ 𝒫 𝐴)) | ||
Theorem | gchdju1 10275 | An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 1o) ≈ 𝐴) | ||
Theorem | gchinf 10276 | An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ω ≼ 𝐴) | ||
Theorem | pwfseqlem1 10277* | Lemma for pwfseq 10283. Derive a contradiction by diagonalization. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐷 ∈ (∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ∖ ∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛))) | ||
Theorem | pwfseqlem2 10278* | Lemma for pwfseq 10283. (Contributed by Mario Carneiro, 18-Nov-2014.) (Revised by AV, 18-Sep-2021.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) ⇒ ⊢ ((𝑌 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑌𝐹𝑅) = (𝐻‘(card‘𝑌))) | ||
Theorem | pwfseqlem3 10279* | Lemma for pwfseq 10283. Using the construction 𝐷 from pwfseqlem1 10277, produce a function 𝐹 that maps any well-ordered infinite set to an element outside the set. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) | ||
Theorem | pwfseqlem4a 10280* | Lemma for pwfseqlem4 10281. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) ⇒ ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴) | ||
Theorem | pwfseqlem4 10281* | Lemma for pwfseq 10283. Derive a final contradiction from the function 𝐹 in pwfseqlem3 10279. Applying fpwwe2 10262 to it, we get a certain maximal well-ordered subset 𝑍, but the defining property (𝑍𝐹(𝑊‘𝑍)) ∈ 𝑍 contradicts our assumption on 𝐹, so we are reduced to the case of 𝑍 finite. This too is a contradiction, though, because 𝑍 and its preimage under (𝑊‘𝑍) are distinct sets of the same cardinality and in a subset relation, which is impossible for finite sets. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑m 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) & ⊢ 𝑊 = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))} & ⊢ 𝑍 = ∪ dom 𝑊 ⇒ ⊢ ¬ 𝜑 | ||
Theorem | pwfseqlem5 10282* |
Lemma for pwfseq 10283. Although in some ways pwfseqlem4 10281 is the "main"
part of the proof, one last aspect which makes up a remark in the
original text is by far the hardest part to formalize. The main proof
relies on the existence of an injection 𝐾 from the set of finite
sequences on an infinite set 𝑥 to 𝑥. Now this alone would
not
be difficult to prove; this is mostly the claim of fseqen 9646. However,
what is needed for the proof is a canonical injection on these
sets,
so we have to start from scratch pulling together explicit bijections
from the lemmas.
If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen 9633. The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms (cnfcom3c 9326), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 9637). (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) & ⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) & ⊢ 𝑂 = OrdIso(𝑟, 𝑡) & ⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉) & ⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇) & ⊢ 𝑆 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑m suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {〈∅, (𝑂‘∅)〉}) & ⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑m 𝑛) ↦ 〈dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)〉) & ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉) & ⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | pwfseq 10283* | The powerset of a Dedekind-infinite set does not inject into the set of finite sequences. The proof is due to Halbeisen and Shelah. Proposition 1.7 of [KanamoriPincus] p. 418. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) | ||
Theorem | pwxpndom2 10284 | The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) (Proof shortened by AV, 18-Jul-2022.) |
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 ⊔ (𝐴 × 𝐴))) | ||
Theorem | pwxpndom 10285 | The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 × 𝐴)) | ||
Theorem | pwdjundom 10286 | The powerset of a Dedekind-infinite set does not inject into its cardinal sum with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 ⊔ 𝐴)) | ||
Theorem | gchdjuidm 10287 | An infinite GCH-set is idempotent under cardinal sum. Part of Lemma 2.2 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 ⊔ 𝐴) ≈ 𝐴) | ||
Theorem | gchxpidm 10288 | An infinite GCH-set is idempotent under cardinal product. Part of Lemma 2.2 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 × 𝐴) ≈ 𝐴) | ||
Theorem | gchpwdom 10289 | A relationship between dominance over the powerset and strict dominance when the sets involved are infinite GCH-sets. Proposition 3.1 of [KanamoriPincus] p. 421. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝐵 ∈ GCH) → (𝐴 ≺ 𝐵 ↔ 𝒫 𝐴 ≼ 𝐵)) | ||
Theorem | gchaleph 10290 | If (ℵ‘𝐴) is a GCH-set and its powerset is well-orderable, then the successor aleph (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴). (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 ∈ On ∧ (ℵ‘𝐴) ∈ GCH ∧ 𝒫 (ℵ‘𝐴) ∈ dom card) → (ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴)) | ||
Theorem | gchaleph2 10291 | If (ℵ‘𝐴) and (ℵ‘suc 𝐴) are GCH-sets, then the successor aleph (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴). (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ ((𝐴 ∈ On ∧ (ℵ‘𝐴) ∈ GCH ∧ (ℵ‘suc 𝐴) ∈ GCH) → (ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴)) | ||
Theorem | hargch 10292 | If 𝐴 + ≈ 𝒫 𝐴, then 𝐴 is a GCH-set. The much simpler converse to gchhar 10298. (Contributed by Mario Carneiro, 2-Jun-2015.) |
⊢ ((har‘𝐴) ≈ 𝒫 𝐴 → 𝐴 ∈ GCH) | ||
Theorem | alephgch 10293 | If (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴), then (ℵ‘𝐴) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴) → (ℵ‘𝐴) ∈ GCH) | ||
Theorem | gch2 10294 | It is sufficient to require that all alephs are GCH-sets to ensure the full generalized continuum hypothesis. (The proof uses the Axiom of Regularity.) (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (GCH = V ↔ ran ℵ ⊆ GCH) | ||
Theorem | gch3 10295 | An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (GCH = V ↔ ∀𝑥 ∈ On (ℵ‘suc 𝑥) ≈ 𝒫 (ℵ‘𝑥)) | ||
Theorem | gch-kn 10296* | The equivalence of two versions of the Generalized Continuum Hypothesis. The right-hand side is the standard version in the literature. The left-hand side is a version devised by Kannan Nambiar, which he calls the Axiom of Combinatorial Sets. For the notation and motivation behind this axiom, see his paper, "Derivation of Continuum Hypothesis from Axiom of Combinatorial Sets", available at http://www.e-atheneum.net/science/derivation_ch.pdf. The equivalence of the two sides provides a negative answer to Open Problem 2 in http://www.e-atheneum.net/science/open_problem_print.pdf. The key idea in the proof below is to equate both sides of alephexp2 10200 to the successor aleph using enen2 8792. (Contributed by NM, 1-Oct-2004.) |
⊢ (𝐴 ∈ On → ((ℵ‘suc 𝐴) ≈ {𝑥 ∣ (𝑥 ⊆ (ℵ‘𝐴) ∧ 𝑥 ≈ (ℵ‘𝐴))} ↔ (ℵ‘suc 𝐴) ≈ (2o ↑m (ℵ‘𝐴)))) | ||
Theorem | gchaclem 10297 | Lemma for gchac 10300 (obsolete, used in Sierpiński's proof). (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝜑 → ω ≼ 𝐴) & ⊢ (𝜑 → 𝒫 𝐶 ∈ GCH) & ⊢ (𝜑 → (𝐴 ≼ 𝐶 ∧ (𝐵 ≼ 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵))) ⇒ ⊢ (𝜑 → (𝐴 ≼ 𝒫 𝐶 ∧ (𝐵 ≼ 𝒫 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵))) | ||
Theorem | gchhar 10298 | A "local" form of gchac 10300. If 𝐴 and 𝒫 𝐴 are GCH-sets, then the Hartogs number of 𝐴 is 𝒫 𝐴 (so 𝒫 𝐴 and a fortiori 𝐴 are well-orderable). The proof is due to Specker. Theorem 2.1 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → (har‘𝐴) ≈ 𝒫 𝐴) | ||
Theorem | gchacg 10299 | A "local" form of gchac 10300. If 𝐴 and 𝒫 𝐴 are GCH-sets, then 𝒫 𝐴 is well-orderable. The proof is due to Specker. Theorem 2.1 of [KanamoriPincus] p. 419. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((ω ≼ 𝐴 ∧ 𝐴 ∈ GCH ∧ 𝒫 𝐴 ∈ GCH) → 𝒫 𝐴 ∈ dom card) | ||
Theorem | gchac 10300 | The Generalized Continuum Hypothesis implies the Axiom of Choice. The original proof is due to Sierpiński (1947); we use a refinement of Sierpiński's result due to Specker. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (GCH = V → CHOICE) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |