Home | Metamath
Proof Explorer Theorem List (p. 94 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | axpowndlem4 9301 | Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → (¬ ∀𝑦 𝑦 = 𝑧 → (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)))) | ||
Theorem | axpownd 9302 | A version of the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.) |
⊢ (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧 𝑥 ∈ 𝑦 → ∀𝑦 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)) | ||
Theorem | axregndlem1 9303 | Lemma for the Axiom of Regularity with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) |
⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))) | ||
Theorem | axregndlem2 9304* | Lemma for the Axiom of Regularity with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) |
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
Theorem | axregnd 9305 | A version of the Axiom of Regularity with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Wolf Lammen, 18-Aug-2019.) |
⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦))) | ||
Theorem | axinfndlem1 9306* | Lemma for the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.) |
⊢ (∀𝑥 𝑦 ∈ 𝑧 → ∃𝑥(𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) | ||
Theorem | axinfnd 9307 | A version of the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.) |
⊢ ∃𝑥(𝑦 ∈ 𝑧 → (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥)))) | ||
Theorem | axacndlem1 9308 | Lemma for the Axiom of Choice with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) | ||
Theorem | axacndlem2 9309 | Lemma for the Axiom of Choice with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) |
⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) | ||
Theorem | axacndlem3 9310 | Lemma for the Axiom of Choice with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) |
⊢ (∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))) | ||
Theorem | axacndlem4 9311* | 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 9312* | 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 9313 | 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 9314* | Axiom of Extensionality ax-ext 2590, reproved from conditionless ZFC version and predicate calculus. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
⊢ (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦) | ||
Theorem | zfcndrep 9315* | Axiom of Replacement ax-rep 4699, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧 ∈ 𝑦 ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))) | ||
Theorem | zfcndun 9316* | Axiom of Union ax-un 6847, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
⊢ ∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfcndpow 9317* | Axiom of Power Sets ax-pow 4769, reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness," dtru 4783. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
⊢ ∃𝑦∀𝑧(∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) | ||
Theorem | zfcndreg 9318* | Axiom of Regularity ax-reg 8380, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
⊢ (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑦(𝑦 ∈ 𝑥 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))) | ||
Theorem | zfcndinf 9319* | Axiom of Infinity ax-inf 8418, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing theorem el 4773 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.) |
⊢ ∃𝑦(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦))) | ||
Theorem | zfcndac 9320* | Axiom of Choice ax-ac 9164, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ∃𝑦∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → ∃𝑣∀𝑢(∃𝑡((𝑢 ∈ 𝑤 ∧ 𝑤 ∈ 𝑡) ∧ (𝑢 ∈ 𝑡 ∧ 𝑡 ∈ 𝑦)) ↔ 𝑢 = 𝑣)) | ||
Syntax | cgch 9321 | Extend class notation to include the collection of sets that satisfy the GCH. |
class GCH | ||
Definition | df-gch 9322* | 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 9323* | Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ GCH ↔ (𝐴 ∈ Fin ∨ ∀𝑥 ¬ (𝐴 ≺ 𝑥 ∧ 𝑥 ≺ 𝒫 𝐴)))) | ||
Theorem | fingch 9324 | A finite set is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ Fin ⊆ GCH | ||
Theorem | gchi 9325 | 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 9326 | If 𝐴 ≤ 𝐵 < 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐴 = 𝐵 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≺ 𝒫 𝐴)) → 𝐴 ≈ 𝐵) | ||
Theorem | gchen2 9327 | If 𝐴 < 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → 𝐵 ≈ 𝒫 𝐴) | ||
Theorem | gchor 9328 | If 𝐴 ≤ 𝐵 ≤ 𝒫 𝐴, and 𝐴 is an infinite GCH-set, then either 𝐴 = 𝐵 or 𝐵 = 𝒫 𝐴 in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝒫 𝐴)) → (𝐴 ≈ 𝐵 ∨ 𝐵 ≈ 𝒫 𝐴)) | ||
Theorem | engch 9329 | The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ GCH ↔ 𝐵 ∈ GCH)) | ||
Theorem | gchdomtri 9330 | Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac 9382. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((𝐴 ∈ GCH ∧ (𝐴 +𝑐 𝐴) ≈ 𝐴 ∧ 𝐵 ≼ 𝒫 𝐴) → (𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴)) | ||
Theorem | fpwwe2cbv 9331* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 3-Jun-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} ⇒ ⊢ 𝑊 = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 [(◡𝑠 “ {𝑧}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑧))} | ||
Theorem | fpwwe2lem1 9332* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} ⇒ ⊢ 𝑊 ⊆ (𝒫 𝐴 × 𝒫 (𝐴 × 𝐴)) | ||
Theorem | fpwwe2lem2 9333* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 19-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) ⇒ ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))) | ||
Theorem | fpwwe2lem3 9334* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 19-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → 𝑋𝑊𝑅) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑋) → ((◡𝑅 “ {𝐵})𝐹(𝑅 ∩ ((◡𝑅 “ {𝐵}) × (◡𝑅 “ {𝐵})))) = 𝐵) | ||
Theorem | fpwwe2lem5 9335* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) ⇒ ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴) | ||
Theorem | fpwwe2lem6 9336* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) & ⊢ 𝑀 = OrdIso(𝑅, 𝑋) & ⊢ 𝑁 = OrdIso(𝑆, 𝑌) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑁) & ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (◡𝑀‘𝐶) = (◡𝑁‘𝐶))) | ||
Theorem | fpwwe2lem7 9337* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) & ⊢ 𝑀 = OrdIso(𝑅, 𝑋) & ⊢ 𝑁 = OrdIso(𝑆, 𝑌) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐵 ∈ dom 𝑁) & ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵)) ⇒ ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶𝑆(𝑁‘𝐵) ∧ (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷)))) | ||
Theorem | fpwwe2lem8 9338* | Lemma for fpwwe2 9344. Show by induction that the two isometries 𝑀 and 𝑁 agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) & ⊢ 𝑀 = OrdIso(𝑅, 𝑋) & ⊢ 𝑁 = OrdIso(𝑆, 𝑌) & ⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) ⇒ ⊢ (𝜑 → 𝑀 = (𝑁 ↾ dom 𝑀)) | ||
Theorem | fpwwe2lem9 9339* | Lemma for fpwwe2 9344. 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.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) & ⊢ 𝑀 = OrdIso(𝑅, 𝑋) & ⊢ 𝑁 = OrdIso(𝑆, 𝑌) & ⊢ (𝜑 → dom 𝑀 ⊆ dom 𝑁) ⇒ ⊢ (𝜑 → (𝑋 ⊆ 𝑌 ∧ 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))) | ||
Theorem | fpwwe2lem10 9340* | Lemma for fpwwe2 9344. Given two well-orders 〈𝑋, 𝑅〉 and 〈𝑌, 𝑆〉 of parts of 𝐴, one is an initial segment of the other. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑊𝑅) & ⊢ (𝜑 → 𝑌𝑊𝑆) ⇒ ⊢ (𝜑 → ((𝑋 ⊆ 𝑌 ∧ 𝑅 = (𝑆 ∩ (𝑌 × 𝑋))) ∨ (𝑌 ⊆ 𝑋 ∧ 𝑆 = (𝑅 ∩ (𝑋 × 𝑌))))) | ||
Theorem | fpwwe2lem11 9341* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → 𝑊:dom 𝑊⟶𝒫 (𝑋 × 𝑋)) | ||
Theorem | fpwwe2lem12 9342* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → 𝑋 ∈ dom 𝑊) | ||
Theorem | fpwwe2lem13 9343* | Lemma for fpwwe2 9344. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → (𝑋𝐹(𝑊‘𝑋)) ∈ 𝑋) | ||
Theorem | fpwwe2 9344* | 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 8736. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌𝐹𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)))) | ||
Theorem | fpwwecbv 9345* | Lemma for fpwwe 9347. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} ⇒ ⊢ 𝑊 = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (𝐹‘(◡𝑠 “ {𝑧})) = 𝑧))} | ||
Theorem | fpwwelem 9346* | Lemma for fpwwe 9347. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) ⇒ ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝐹‘(◡𝑅 “ {𝑦})) = 𝑦)))) | ||
Theorem | fpwwe 9347* | Given any function 𝐹 from the powerset of 𝐴 to 𝐴, canth2 7998 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 8736. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹‘𝑥) ∈ 𝐴) & ⊢ 𝑋 = ∪ dom 𝑊 ⇒ ⊢ (𝜑 → ((𝑌𝑊𝑅 ∧ (𝐹‘𝑌) ∈ 𝑌) ↔ (𝑌 = 𝑋 ∧ 𝑅 = (𝑊‘𝑋)))) | ||
Theorem | canth4 9348* | An "effective" form of Cantor's theorem canth 6508. 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 9349* | Lemma for canthnum 9350. (Contributed by Mario Carneiro, 19-May-2015.) |
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐹‘(◡𝑟 “ {𝑦})) = 𝑦))} & ⊢ 𝐵 = ∪ dom 𝑊 & ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐹‘𝐵)}) ⇒ ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:(𝒫 𝐴 ∩ dom card)–1-1→𝐴) | ||
Theorem | canthnum 9350 | The set of well-orderable subsets of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 7998. Corollary 1.4(a) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 19-May-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ (𝒫 𝐴 ∩ dom card)) | ||
Theorem | canthwelem 9351* | Lemma for canthnum 9350. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ 𝑂 = {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} & ⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} & ⊢ 𝐵 = ∪ dom 𝑊 & ⊢ 𝐶 = (◡(𝑊‘𝐵) “ {(𝐵𝐹(𝑊‘𝐵))}) ⇒ ⊢ (𝐴 ∈ 𝑉 → ¬ 𝐹:𝑂–1-1→𝐴) | ||
Theorem | canthwe 9352* | The set of well-orders of a set 𝐴 strictly dominates 𝐴. A stronger form of canth2 7998. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ 𝑂 = {〈𝑥, 𝑟〉 ∣ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≺ 𝑂) | ||
Theorem | canthp1lem1 9353 | Lemma for canthp1 9355. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (1𝑜 ≺ 𝐴 → (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴) | ||
Theorem | canthp1lem2 9354* | Lemma for canthp1 9355. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ (𝜑 → 1𝑜 ≺ 𝐴) & ⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→(𝐴 +𝑐 1𝑜)) & ⊢ (𝜑 → 𝐺:((𝐴 +𝑐 1𝑜) ∖ {(𝐹‘𝐴)})–1-1-onto→𝐴) & ⊢ 𝐻 = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) & ⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐻‘(◡𝑟 “ {𝑦})) = 𝑦))} & ⊢ 𝐵 = ∪ dom 𝑊 ⇒ ⊢ ¬ 𝜑 | ||
Theorem | canthp1 9355 | 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.) |
⊢ (1𝑜 ≺ 𝐴 → (𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴) | ||
Theorem | finngch 9356 | The exclusion of finite sets from consideration in df-gch 9322 is necessary, because otherwise finite sets larger than a singleton would violate the GCH property. (Contributed by Mario Carneiro, 10-Jun-2015.) |
⊢ ((𝐴 ∈ Fin ∧ 1𝑜 ≺ 𝐴) → (𝐴 ≺ (𝐴 +𝑐 1𝑜) ∧ (𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴)) | ||
Theorem | gchcda1 9357 | An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015.) |
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → (𝐴 +𝑐 1𝑜) ≈ 𝐴) | ||
Theorem | gchinf 9358 | An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ ((𝐴 ∈ GCH ∧ ¬ 𝐴 ∈ Fin) → ω ≼ 𝐴) | ||
Theorem | pwfseqlem1 9359* | Lemma for pwfseq 9365. Derive a contradiction by diagonalization. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑𝑚 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝐷 ∈ (∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∖ ∪ 𝑛 ∈ ω (𝑥 ↑𝑚 𝑛))) | ||
Theorem | pwfseqlem2 9360* | Lemma for pwfseq 9365. (Contributed by Mario Carneiro, 18-Nov-2014.) (Revised by AV, 18-Sep-2021.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑𝑚 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) ⇒ ⊢ ((𝑌 ∈ Fin ∧ 𝑅 ∈ 𝑉) → (𝑌𝐹𝑅) = (𝐻‘(card‘𝑌))) | ||
Theorem | pwfseqlem3 9361* | Lemma for pwfseq 9365. Using the construction 𝐷 from pwfseqlem1 9359, 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→∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑𝑚 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑥𝐹𝑟) ∈ (𝐴 ∖ 𝑥)) | ||
Theorem | pwfseqlem4a 9362* | Lemma for pwfseqlem4 9363. (Contributed by Mario Carneiro, 7-Jun-2016.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑𝑚 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) ⇒ ⊢ ((𝜑 ∧ (𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎) ∧ 𝑠 We 𝑎)) → (𝑎𝐹𝑠) ∈ 𝐴) | ||
Theorem | pwfseqlem4 9363* | Lemma for pwfseq 9365. Derive a final contradiction from the function 𝐹 in pwfseqlem3 9361. Applying fpwwe2 9344 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→∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ∧ ω ≼ 𝑥)) & ⊢ ((𝜑 ∧ 𝜓) → 𝐾:∪ 𝑛 ∈ ω (𝑥 ↑𝑚 𝑛)–1-1→𝑥) & ⊢ 𝐷 = (𝐺‘{𝑤 ∈ 𝑥 ∣ ((◡𝐾‘𝑤) ∈ ran 𝐺 ∧ ¬ 𝑤 ∈ (◡𝐺‘(◡𝐾‘𝑤)))}) & ⊢ 𝐹 = (𝑥 ∈ V, 𝑟 ∈ V ↦ if(𝑥 ∈ Fin, (𝐻‘(card‘𝑥)), (𝐷‘∩ {𝑧 ∈ ω ∣ ¬ (𝐷‘𝑧) ∈ 𝑥}))) & ⊢ 𝑊 = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑏 ∈ 𝑎 [(◡𝑠 “ {𝑏}) / 𝑣](𝑣𝐹(𝑠 ∩ (𝑣 × 𝑣))) = 𝑏))} & ⊢ 𝑍 = ∪ dom 𝑊 ⇒ ⊢ ¬ 𝜑 | ||
Theorem | pwfseqlem5 9364* |
Lemma for pwfseq 9365. Although in some ways pwfseqlem4 9363 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 8733. 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 8720. 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 8486), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 8724). (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (𝜑 → 𝐺:𝒫 𝐴–1-1→∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) & ⊢ (𝜑 → 𝑋 ⊆ 𝐴) & ⊢ (𝜑 → 𝐻:ω–1-1-onto→𝑋) & ⊢ (𝜓 ↔ ((𝑡 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑡 × 𝑡) ∧ 𝑟 We 𝑡) ∧ ω ≼ 𝑡)) & ⊢ (𝜑 → ∀𝑏 ∈ (har‘𝒫 𝐴)(ω ⊆ 𝑏 → (𝑁‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) & ⊢ 𝑂 = OrdIso(𝑟, 𝑡) & ⊢ 𝑇 = (𝑢 ∈ dom 𝑂, 𝑣 ∈ dom 𝑂 ↦ 〈(𝑂‘𝑢), (𝑂‘𝑣)〉) & ⊢ 𝑃 = ((𝑂 ∘ (𝑁‘dom 𝑂)) ∘ ◡𝑇) & ⊢ 𝑆 = seq𝜔((𝑘 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝑡 ↑𝑚 suc 𝑘) ↦ ((𝑓‘(𝑥 ↾ 𝑘))𝑃(𝑥‘𝑘)))), {〈∅, (𝑂‘∅)〉}) & ⊢ 𝑄 = (𝑦 ∈ ∪ 𝑛 ∈ ω (𝑡 ↑𝑚 𝑛) ↦ 〈dom 𝑦, ((𝑆‘dom 𝑦)‘𝑦)〉) & ⊢ 𝐼 = (𝑥 ∈ ω, 𝑦 ∈ 𝑡 ↦ 〈(𝑂‘𝑥), 𝑦〉) & ⊢ 𝐾 = ((𝑃 ∘ 𝐼) ∘ 𝑄) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | pwfseq 9365* | 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.) |
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) | ||
Theorem | pwxpndom2 9366 | The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 +𝑐 (𝐴 × 𝐴))) | ||
Theorem | pwxpndom 9367 | The powerset of a Dedekind-infinite set does not inject into its Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 × 𝐴)) | ||
Theorem | pwcdandom 9368 | The powerset of a Dedekind-infinite set does not inject into its cardinal sum with itself. (Contributed by Mario Carneiro, 31-May-2015.) |
⊢ (ω ≼ 𝐴 → ¬ 𝒫 𝐴 ≼ (𝐴 +𝑐 𝐴)) | ||
Theorem | gchcdaidm 9369 | 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 9370 | 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 9371 | 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 9372 | 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 9373 | 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 9374 | If 𝐴 + ≈ 𝒫 𝐴, then 𝐴 is a GCH-set. The much simpler converse to gchhar 9380. (Contributed by Mario Carneiro, 2-Jun-2015.) |
⊢ ((har‘𝐴) ≈ 𝒫 𝐴 → 𝐴 ∈ GCH) | ||
Theorem | alephgch 9375 | If (ℵ‘suc 𝐴) is equinumerous to the powerset of (ℵ‘𝐴), then (ℵ‘𝐴) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ ((ℵ‘suc 𝐴) ≈ 𝒫 (ℵ‘𝐴) → (ℵ‘𝐴) ∈ GCH) | ||
Theorem | gch2 9376 | 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 9377 | An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (GCH = V ↔ ∀𝑥 ∈ On (ℵ‘suc 𝑥) ≈ 𝒫 (ℵ‘𝑥)) | ||
Theorem | gch-kn 9378* | 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 9282 to the successor aleph using enen2 7986. (Contributed by NM, 1-Oct-2004.) |
⊢ (𝐴 ∈ On → ((ℵ‘suc 𝐴) ≈ {𝑥 ∣ (𝑥 ⊆ (ℵ‘𝐴) ∧ 𝑥 ≈ (ℵ‘𝐴))} ↔ (ℵ‘suc 𝐴) ≈ (2𝑜 ↑𝑚 (ℵ‘𝐴)))) | ||
Theorem | gchaclem 9379 | Lemma for gchac 9382 (obsolete, used in Sierpiński's proof). (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝜑 → ω ≼ 𝐴) & ⊢ (𝜑 → 𝒫 𝐶 ∈ GCH) & ⊢ (𝜑 → (𝐴 ≼ 𝐶 ∧ (𝐵 ≼ 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵))) ⇒ ⊢ (𝜑 → (𝐴 ≼ 𝒫 𝐶 ∧ (𝐵 ≼ 𝒫 𝒫 𝐶 → 𝒫 𝐴 ≼ 𝐵))) | ||
Theorem | gchhar 9380 | A "local" form of gchac 9382. 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 9381 | A "local" form of gchac 9382. 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 9382 | 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) | ||
Here we introduce Tarski-Grothendieck (TG) set theory, named after mathematicians Alfred Tarski and Alexander Grothendieck. TG theory extends ZFC with the TG Axiom ax-groth 9524, which states that for every set 𝑥 there is an inaccessible cardinal 𝑦 such that 𝑦 is not in 𝑥. The addition of this axiom to ZFC set theory provides a framework for category theory, thus for all practical purposes giving us a complete foundation for "all of mathematics." We first introduce the concept of inaccessibles, including weakly and strongly inaccessible cardinals (df-wina 9385 and df-ina 9386 respectively ), Tarski classes (df-tsk 9450), and Grothendieck universes (df-gru 9492). We then introduce the Tarski's axiom ax-groth 9524 and prove various properties from that. | ||
Syntax | cwina 9383 | The class of weak inaccessibles. |
class Inaccw | ||
Syntax | cina 9384 | The class of strong inaccessibles. |
class Inacc | ||
Definition | df-wina 9385* | An ordinal is weakly inaccessible iff it is a regular limit cardinal. Note that our definition allows ω as a weakly inaccessible cardinal. (Contributed by Mario Carneiro, 22-Jun-2013.) |
⊢ Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝑥 𝑦 ≺ 𝑧)} | ||
Definition | df-ina 9386* | An ordinal is strongly inaccessible iff it is a regular strong limit cardinal, which is to say that it dominates the powersets of every smaller ordinal. (Contributed by Mario Carneiro, 22-Jun-2013.) |
⊢ Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥)} | ||
Theorem | elwina 9387* | Conditions of weak inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
⊢ (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) | ||
Theorem | elina 9388* | Conditions of strong inaccessibility. (Contributed by Mario Carneiro, 22-Jun-2013.) |
⊢ (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴)) | ||
Theorem | winaon 9389 | A weakly inaccessible cardinal is an ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inaccw → 𝐴 ∈ On) | ||
Theorem | inawinalem 9390* | Lemma for inawina 9391. (Contributed by Mario Carneiro, 8-Jun-2014.) |
⊢ (𝐴 ∈ On → (∀𝑥 ∈ 𝐴 𝒫 𝑥 ≺ 𝐴 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) | ||
Theorem | inawina 9391 | Every strongly inaccessible cardinal is weakly inaccessible. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw) | ||
Theorem | omina 9392 | ω is a strongly inaccessible cardinal. (Many definitions of "inaccessible" explicitly disallow ω as an inaccessible cardinal, but this choice allows us to reuse our results for inaccessibles for ω.) (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ ω ∈ Inacc | ||
Theorem | winacard 9393 | A weakly inaccessible cardinal is a cardinal. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴) | ||
Theorem | winainflem 9394* | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ω ⊆ 𝐴) | ||
Theorem | winainf 9395 | A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴) | ||
Theorem | winalim 9396 | A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ (𝐴 ∈ Inaccw → Lim 𝐴) | ||
Theorem | winalim2 9397* | A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)) | ||
Theorem | winafp 9398 | A nontrivial weakly inaccessible cardinal is a fixed point of the aleph function. (Contributed by Mario Carneiro, 29-May-2014.) |
⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → (ℵ‘𝐴) = 𝐴) | ||
Theorem | winafpi 9399 | This theorem, which states that a nontrivial inaccessible cardinal is its own aleph number, is stated here in inference form, where the assumptions are in the hypotheses rather than an antecedent. Often, we use dedth 4089 to turn this type of statement into the closed form statement winafp 9398, but in this case, since it is consistent with ZFC that there are no nontrivial inaccessible cardinals, it is not possible to prove winafp 9398 using this theorem and dedth 4089, in ZFC. (You can prove this if you use ax-groth 9524, though.) (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ 𝐴 ∈ Inaccw & ⊢ 𝐴 ≠ ω ⇒ ⊢ (ℵ‘𝐴) = 𝐴 | ||
Theorem | gchina 9400 | Assuming the GCH, weakly and strongly inaccessible cardinals coincide. Theorem 11.20 of [TakeutiZaring] p. 106. (Contributed by Mario Carneiro, 5-Jun-2015.) |
⊢ (GCH = V → Inaccw = Inacc) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |