![]() |
Metamath
Proof Explorer Theorem List (p. 107 of 482) | < 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: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | smobeth 10601 | 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 10602 | A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.) |
β’ (βπ₯ π₯ = π¦ β Β¬ βπ₯ π¦ β π§) | ||
Theorem | nd2 10603 | A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 1-Jan-2002.) (New usage is discouraged.) |
β’ (βπ₯ π₯ = π¦ β Β¬ βπ₯ π§ β π¦) | ||
Theorem | nd3 10604 | A lemma for proving conditionless ZFC axioms. (Contributed by NM, 2-Jan-2002.) |
β’ (βπ₯ π₯ = π¦ β Β¬ βπ§ π₯ β π¦) | ||
Theorem | nd4 10605 | A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
β’ (βπ₯ π₯ = π¦ β Β¬ βπ§ π¦ β π₯) | ||
Theorem | axextnd 10606 | A version of the Axiom of Extensionality with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 14-Aug-2003.) (New usage is discouraged.) |
β’ βπ₯((π₯ β π¦ β π₯ β π§) β π¦ = π§) | ||
Theorem | axrepndlem1 10607* | Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
β’ (Β¬ βπ¦ π¦ = π§ β βπ₯(βπ¦βπ§(π β π§ = π¦) β βπ§(π§ β π₯ β βπ₯(π₯ β π¦ β§ βπ¦π)))) | ||
Theorem | axrepndlem2 10608 | Lemma for the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (New usage is discouraged.) |
β’ (((Β¬ βπ₯ π₯ = π¦ β§ Β¬ βπ₯ π₯ = π§) β§ Β¬ βπ¦ π¦ = π§) β βπ₯(βπ¦βπ§(π β π§ = π¦) β βπ§(π§ β π₯ β βπ₯(π₯ β π¦ β§ βπ¦π)))) | ||
Theorem | axrepnd 10609 | A version of the Axiom of Replacement with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
β’ βπ₯(βπ¦βπ§(π β π§ = π¦) β βπ§(βπ¦ π§ β π₯ β βπ₯(βπ§ π₯ β π¦ β§ βπ¦π))) | ||
Theorem | axunndlem1 10610* | Lemma for the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
β’ βπ₯βπ¦(βπ₯(π¦ β π₯ β§ π₯ β π§) β π¦ β π₯) | ||
Theorem | axunnd 10611 | A version of the Axiom of Union with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.) |
β’ βπ₯βπ¦(βπ₯(π¦ β π₯ β§ π₯ β π§) β π¦ β π₯) | ||
Theorem | axpowndlem1 10612 | Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.) |
β’ (βπ₯ π₯ = π¦ β (Β¬ π₯ = π¦ β βπ₯βπ¦(βπ₯(βπ§ π₯ β π¦ β βπ¦ π₯ β π§) β π¦ β π₯))) | ||
Theorem | axpowndlem2 10613* | 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 2366. (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 10614* | Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (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 10615 | Lemma for the Axiom of Power Sets with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) (New usage is discouraged.) |
β’ (Β¬ βπ¦ π¦ = π₯ β (Β¬ βπ¦ π¦ = π§ β (Β¬ π₯ = π¦ β βπ₯βπ¦(βπ₯(βπ§ π₯ β π¦ β βπ¦ π₯ β π§) β π¦ β π₯)))) | ||
Theorem | axpownd 10616 | 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 2366. (Contributed by NM, 4-Jan-2002.) (New usage is discouraged.) |
β’ (Β¬ π₯ = π¦ β βπ₯βπ¦(βπ₯(βπ§ π₯ β π¦ β βπ¦ π₯ β π§) β π¦ β π₯)) | ||
Theorem | axregndlem1 10617 | Lemma for the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.) |
β’ (βπ₯ π₯ = π§ β (π₯ β π¦ β βπ₯(π₯ β π¦ β§ βπ§(π§ β π₯ β Β¬ π§ β π¦)))) | ||
Theorem | axregndlem2 10618* | Lemma for the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.) (New usage is discouraged.) |
β’ (π₯ β π¦ β βπ₯(π₯ β π¦ β§ βπ§(π§ β π₯ β Β¬ π§ β π¦))) | ||
Theorem | axregnd 10619 | A version of the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Jan-2002.) (Proof shortened by Wolf Lammen, 18-Aug-2019.) (New usage is discouraged.) |
β’ (π₯ β π¦ β βπ₯(π₯ β π¦ β§ βπ§(π§ β π₯ β Β¬ π§ β π¦))) | ||
Theorem | axinfndlem1 10620* | Lemma for the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.) |
β’ (βπ₯ π¦ β π§ β βπ₯(π¦ β π₯ β§ βπ¦(π¦ β π₯ β βπ§(π¦ β π§ β§ π§ β π₯)))) | ||
Theorem | axinfnd 10621 | A version of the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.) |
β’ βπ₯(π¦ β π§ β (π¦ β π₯ β§ βπ¦(π¦ β π₯ β βπ§(π¦ β π§ β§ π§ β π₯)))) | ||
Theorem | axacndlem1 10622 | Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.) |
β’ (βπ₯ π₯ = π¦ β βπ₯βπ¦βπ§(βπ₯(π¦ β π§ β§ π§ β π€) β βπ€βπ¦(βπ€((π¦ β π§ β§ π§ β π€) β§ (π¦ β π€ β§ π€ β π₯)) β π¦ = π€))) | ||
Theorem | axacndlem2 10623 | Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.) |
β’ (βπ₯ π₯ = π§ β βπ₯βπ¦βπ§(βπ₯(π¦ β π§ β§ π§ β π€) β βπ€βπ¦(βπ€((π¦ β π§ β§ π§ β π€) β§ (π¦ β π€ β§ π€ β π₯)) β π¦ = π€))) | ||
Theorem | axacndlem3 10624 | Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Jan-2002.) (New usage is discouraged.) |
β’ (βπ¦ π¦ = π§ β βπ₯βπ¦βπ§(βπ₯(π¦ β π§ β§ π§ β π€) β βπ€βπ¦(βπ€((π¦ β π§ β§ π§ β π€) β§ (π¦ β π€ β§ π€ β π₯)) β π¦ = π€))) | ||
Theorem | axacndlem4 10625* | 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 10626* | 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 10627 | 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 10628* | Axiom of Extensionality ax-ext 2698, reproved from conditionless ZFC version and predicate calculus. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ§(π§ β π₯ β π§ β π¦) β π₯ = π¦) | ||
Theorem | zfcndrep 10629* | Axiom of Replacement ax-rep 5279, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ€βπ¦βπ§(βπ¦π β π§ = π¦) β βπ¦βπ§(π§ β π¦ β βπ€(π€ β π₯ β§ βπ¦π))) | ||
Theorem | zfcndun 10630* | Axiom of Union ax-un 7734, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ βπ¦βπ§(βπ€(π§ β π€ β§ π€ β π₯) β π§ β π¦) | ||
Theorem | zfcndpow 10631* | Axiom of Power Sets ax-pow 5359, reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness" dtru 5432. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ βπ¦βπ§(βπ€(π€ β π§ β π€ β π₯) β π§ β π¦) | ||
Theorem | zfcndreg 10632* | Axiom of Regularity ax-reg 9607, reproved from conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (βπ¦ π¦ β π₯ β βπ¦(π¦ β π₯ β§ βπ§(π§ β π¦ β Β¬ π§ β π₯))) | ||
Theorem | zfcndinf 10633* | Axiom of Infinity ax-inf 9653, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing Theorem el 5433 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.) |
β’ βπ¦(π₯ β π¦ β§ βπ§(π§ β π¦ β βπ€(π§ β π€ β§ π€ β π¦))) | ||
Theorem | zfcndac 10634* | Axiom of Choice ax-ac 10474, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ βπ¦βπ§βπ€((π§ β π€ β§ π€ β π₯) β βπ£βπ’(βπ‘((π’ β π€ β§ π€ β π‘) β§ (π’ β π‘ β§ π‘ β π¦)) β π’ = π£)) | ||
Syntax | cgch 10635 | Extend class notation to include the collection of sets that satisfy the GCH. |
class GCH | ||
Definition | df-gch 10636* | 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 10637* | Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π΄ β π β (π΄ β GCH β (π΄ β Fin β¨ βπ₯ Β¬ (π΄ βΊ π₯ β§ π₯ βΊ π« π΄)))) | ||
Theorem | fingch 10638 | A finite set is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ Fin β GCH | ||
Theorem | gchi 10639 | 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 10640 | If π΄ β€ π΅ < π« π΄, and π΄ is an infinite GCH-set, then π΄ = π΅ in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (((π΄ β GCH β§ Β¬ π΄ β Fin) β§ (π΄ βΌ π΅ β§ π΅ βΊ π« π΄)) β π΄ β π΅) | ||
Theorem | gchen2 10641 | If π΄ < π΅ β€ π« π΄, and π΄ is an infinite GCH-set, then π΅ = π« π΄ in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (((π΄ β GCH β§ Β¬ π΄ β Fin) β§ (π΄ βΊ π΅ β§ π΅ βΌ π« π΄)) β π΅ β π« π΄) | ||
Theorem | gchor 10642 | If π΄ β€ π΅ β€ π« π΄, and π΄ is an infinite GCH-set, then either π΄ = π΅ or π΅ = π« π΄ in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (((π΄ β GCH β§ Β¬ π΄ β Fin) β§ (π΄ βΌ π΅ β§ π΅ βΌ π« π΄)) β (π΄ β π΅ β¨ π΅ β π« π΄)) | ||
Theorem | engch 10643 | The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π΄ β π΅ β (π΄ β GCH β π΅ β GCH)) | ||
Theorem | gchdomtri 10644 | Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac 10696. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ ((π΄ β GCH β§ (π΄ β π΄) β π΄ β§ π΅ βΌ π« π΄) β (π΄ βΌ π΅ β¨ π΅ βΌ π΄)) | ||
Theorem | fpwwe2cbv 10645* | Lemma for fpwwe2 10658. (Contributed by Mario Carneiro, 3-Jun-2015.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} β β’ π = {β¨π, π β© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ§ β π [(β‘π β {π§}) / π£](π£πΉ(π β© (π£ Γ π£))) = π§))} | ||
Theorem | fpwwe2lem1 10646* | Lemma for fpwwe2 10658. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} β β’ π β (π« π΄ Γ π« (π΄ Γ π΄)) | ||
Theorem | fpwwe2lem2 10647* | Lemma for fpwwe2 10658. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) β β’ (π β (πππ β ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ¦ β π [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦)))) | ||
Theorem | fpwwe2lem3 10648* | Lemma for fpwwe2 10658. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ (π β πππ ) β β’ ((π β§ π΅ β π) β ((β‘π β {π΅})πΉ(π β© ((β‘π β {π΅}) Γ (β‘π β {π΅})))) = π΅) | ||
Theorem | fpwwe2lem4 10649* | Lemma for fpwwe2 10658. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) β β’ ((π β§ (π β π΄ β§ π β (π Γ π) β§ π We π)) β (ππΉπ ) β π΄) | ||
Theorem | fpwwe2lem5 10650* | Lemma for fpwwe2 10658. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ (π β πππ ) & β’ (π β πππ) & β’ π = OrdIso(π , π) & β’ π = OrdIso(π, π) & β’ (π β π΅ β dom π) & β’ (π β π΅ β dom π) & β’ (π β (π βΎ π΅) = (π βΎ π΅)) β β’ ((π β§ πΆπ (πβπ΅)) β (πΆ β π β§ πΆ β π β§ (β‘πβπΆ) = (β‘πβπΆ))) | ||
Theorem | fpwwe2lem6 10651* | Lemma for fpwwe2 10658. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ (π β πππ ) & β’ (π β πππ) & β’ π = OrdIso(π , π) & β’ π = OrdIso(π, π) & β’ (π β π΅ β dom π) & β’ (π β π΅ β dom π) & β’ (π β (π βΎ π΅) = (π βΎ π΅)) β β’ ((π β§ πΆπ (πβπ΅)) β (πΆπ(πβπ΅) β§ (π·π (πβπ΅) β (πΆπ π· β πΆππ·)))) | ||
Theorem | fpwwe2lem7 10652* | Lemma for fpwwe2 10658. 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 10653* | Lemma for fpwwe2 10658. 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 10654* | Lemma for fpwwe2 10658. 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 10655* | Lemma for fpwwe2 10658. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ π = βͺ dom π β β’ (π β π:dom πβΆπ« (π Γ π)) | ||
Theorem | fpwwe2lem11 10656* | Lemma for fpwwe2 10658. (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 10657* | Lemma for fpwwe2 10658. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)) β (π₯πΉπ) β π΄) & β’ π = βͺ dom π β β’ (π β (ππΉ(πβπ)) β π) | ||
Theorem | fpwwe2 10658* | 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 10045. 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 10659* | Lemma for fpwwe 10661. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (πΉβ(β‘π β {π¦})) = π¦))} β β’ π = {β¨π, π β© β£ ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ§ β π (πΉβ(β‘π β {π§})) = π§))} | ||
Theorem | fpwwelem 10660* | Lemma for fpwwe 10661. (Contributed by Mario Carneiro, 15-May-2015.) (Revised by AV, 20-Jul-2024.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (πΉβ(β‘π β {π¦})) = π¦))} & β’ (π β π΄ β π) β β’ (π β (πππ β ((π β π΄ β§ π β (π Γ π)) β§ (π We π β§ βπ¦ β π (πΉβ(β‘π β {π¦})) = π¦)))) | ||
Theorem | fpwwe 10661* | Given any function πΉ from the powerset of π΄ to π΄, canth2 9146 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 10045. 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 10662* | An "effective" form of Cantor's theorem canth 7367. 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 10663* | Lemma for canthnum 10664. (Contributed by Mario Carneiro, 19-May-2015.) |
β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (πΉβ(β‘π β {π¦})) = π¦))} & β’ π΅ = βͺ dom π & β’ πΆ = (β‘(πβπ΅) β {(πΉβπ΅)}) β β’ (π΄ β π β Β¬ πΉ:(π« π΄ β© dom card)β1-1βπ΄) | ||
Theorem | canthnum 10664 | The set of well-orderable subsets of a set π΄ strictly dominates π΄. A stronger form of canth2 9146. Corollary 1.4(a) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 19-May-2015.) |
β’ (π΄ β π β π΄ βΊ (π« π΄ β© dom card)) | ||
Theorem | canthwelem 10665* | Lemma for canthwe 10666. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ π = {β¨π₯, πβ© β£ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)} & β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ [(β‘π β {π¦}) / π’](π’πΉ(π β© (π’ Γ π’))) = π¦))} & β’ π΅ = βͺ dom π & β’ πΆ = (β‘(πβπ΅) β {(π΅πΉ(πβπ΅))}) β β’ (π΄ β π β Β¬ πΉ:πβ1-1βπ΄) | ||
Theorem | canthwe 10666* | The set of well-orders of a set π΄ strictly dominates π΄. A stronger form of canth2 9146. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ π = {β¨π₯, πβ© β£ (π₯ β π΄ β§ π β (π₯ Γ π₯) β§ π We π₯)} β β’ (π΄ β π β π΄ βΊ π) | ||
Theorem | canthp1lem1 10667 | Lemma for canthp1 10669. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (1o βΊ π΄ β (π΄ β 2o) βΌ π« π΄) | ||
Theorem | canthp1lem2 10668* | Lemma for canthp1 10669. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ (π β 1o βΊ π΄) & β’ (π β πΉ:π« π΄β1-1-ontoβ(π΄ β 1o)) & β’ (π β πΊ:((π΄ β 1o) β {(πΉβπ΄)})β1-1-ontoβπ΄) & β’ π» = ((πΊ β πΉ) β (π₯ β π« π΄ β¦ if(π₯ = π΄, β , π₯))) & β’ π = {β¨π₯, πβ© β£ ((π₯ β π΄ β§ π β (π₯ Γ π₯)) β§ (π We π₯ β§ βπ¦ β π₯ (π»β(β‘π β {π¦})) = π¦))} & β’ π΅ = βͺ dom π β β’ Β¬ π | ||
Theorem | canthp1 10669 | 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 10670 | The exclusion of finite sets from consideration in df-gch 10636 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 10671 | An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015.) |
β’ ((π΄ β GCH β§ Β¬ π΄ β Fin) β (π΄ β 1o) β π΄) | ||
Theorem | gchinf 10672 | An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015.) |
β’ ((π΄ β GCH β§ Β¬ π΄ β Fin) β Ο βΌ π΄) | ||
Theorem | pwfseqlem1 10673* | Lemma for pwfseq 10679. 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 10674* | Lemma for pwfseq 10679. (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 10675* | Lemma for pwfseq 10679. Using the construction π· from pwfseqlem1 10673, 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 10676* | Lemma for pwfseqlem4 10677. (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 10677* | Lemma for pwfseq 10679. Derive a final contradiction from the function πΉ in pwfseqlem3 10675. Applying fpwwe2 10658 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 10678* |
Lemma for pwfseq 10679. Although in some ways pwfseqlem4 10677 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 10042. 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 10029. 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 9721), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 10033). (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 10679* | 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 10680 | 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 10681 | 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 10682 | 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 10683 | 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 10684 | 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 10685 | 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 10686 | 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 10687 | 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 10688 | If π΄ + β π« π΄, then π΄ is a GCH-set. The much simpler converse to gchhar 10694. (Contributed by Mario Carneiro, 2-Jun-2015.) |
β’ ((harβπ΄) β π« π΄ β π΄ β GCH) | ||
Theorem | alephgch 10689 | If (β΅βsuc π΄) is equinumerous to the powerset of (β΅βπ΄), then (β΅βπ΄) is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ ((β΅βsuc π΄) β π« (β΅βπ΄) β (β΅βπ΄) β GCH) | ||
Theorem | gch2 10690 | 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 10691 | An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (GCH = V β βπ₯ β On (β΅βsuc π₯) β π« (β΅βπ₯)) | ||
Theorem | gch-kn 10692* | 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 10596 to the successor aleph using enen2 9134. (Contributed by NM, 1-Oct-2004.) |
β’ (π΄ β On β ((β΅βsuc π΄) β {π₯ β£ (π₯ β (β΅βπ΄) β§ π₯ β (β΅βπ΄))} β (β΅βsuc π΄) β (2o βm (β΅βπ΄)))) | ||
Theorem | gchaclem 10693 | Lemma for gchac 10696 (obsolete, used in SierpiΕski's proof). (Contributed by Mario Carneiro, 15-May-2015.) |
β’ (π β Ο βΌ π΄) & β’ (π β π« πΆ β GCH) & β’ (π β (π΄ βΌ πΆ β§ (π΅ βΌ π« πΆ β π« π΄ βΌ π΅))) β β’ (π β (π΄ βΌ π« πΆ β§ (π΅ βΌ π« π« πΆ β π« π΄ βΌ π΅))) | ||
Theorem | gchhar 10694 | A "local" form of gchac 10696. 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 10695 | A "local" form of gchac 10696. 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 10696 | 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 10838, 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 10699 and df-ina 10700 respectively ), Tarski classes (df-tsk 10764), and Grothendieck universes (df-gru 10806). We then introduce the Tarski's axiom ax-groth 10838 and prove various properties from that. | ||
Syntax | cwina 10697 | The class of weak inaccessibles. |
class Inaccw | ||
Syntax | cina 10698 | The class of strong inaccessibles. |
class Inacc | ||
Definition | df-wina 10699* | 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 10700* | 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βπ₯) = π₯ β§ βπ¦ β π₯ π« π¦ βΊ π₯)} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |