Home | Metamath
Proof Explorer Theorem List (p. 95 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | alephexp1 9401 | An exponentiation law for alephs. Lemma 6.1 of [Jech] p. 42. (Contributed by NM, 29-Sep-2004.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | alephsuc3 9402* | An alternate representation of a successor aleph. Compare alephsuc 8891 and alephsuc2 8903. Equality can be obtained by taking the of the right-hand side then using alephcard 8893 and carden 9373. (Contributed by NM, 23-Oct-2004.) |
Theorem | alephexp2 9403* | An expression equinumerous to 2 to an aleph power. The proof equates the two laws for cardinal exponentiation alephexp1 9401 (which works if the base is less than or equal to the exponent) and infmap 9398 (which works if the exponent is less than or equal to the base). They can be equated only when the base is equal to the exponent, and this is the result. (Contributed by NM, 23-Oct-2004.) |
Theorem | alephreg 9404 | A successor aleph is regular. Theorem 11.15 of [TakeutiZaring] p. 103. (Contributed by Mario Carneiro, 9-Mar-2013.) |
Theorem | pwcfsdom 9405* | A corollary of Konig's Theorem konigth 9391. Theorem 11.28 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.) |
har | ||
Theorem | cfpwsdom 9406 | A corollary of Konig's Theorem konigth 9391. Theorem 11.29 of [TakeutiZaring] p. 108. (Contributed by Mario Carneiro, 20-Mar-2013.) |
Theorem | alephom 9407 | From canth2 8113, we know that , but we cannot prove that (this is the Continuum Hypothesis), nor can we prove that it is less than any bound whatsoever (i.e. the statement is consistent for any ordinal ). However, we can prove that is not equal to , nor , on cofinality grounds, because by Konig's Theorem konigth 9391 (in the form of cfpwsdom 9406), has uncountable cofinality, which eliminates limit alephs like . (The first limit aleph that is not eliminated is , which has cofinality .) (Contributed by Mario Carneiro, 21-Mar-2013.) |
Theorem | smobeth 9408 | The beth function is strictly monotone. This function is not strictly the beth function, but rather bethA is the same as , 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.) |
Theorem | nd1 9409 | A lemma for proving conditionless ZFC axioms. (Contributed by NM, 1-Jan-2002.) |
Theorem | nd2 9410 | A lemma for proving conditionless ZFC axioms. (Contributed by NM, 1-Jan-2002.) |
Theorem | nd3 9411 | A lemma for proving conditionless ZFC axioms. (Contributed by NM, 2-Jan-2002.) |
Theorem | nd4 9412 | A lemma for proving conditionless ZFC axioms. (Contributed by NM, 2-Jan-2002.) |
Theorem | axextnd 9413 | A version of the Axiom of Extensionality with no distinct variable conditions. (Contributed by NM, 14-Aug-2003.) |
Theorem | axrepndlem1 9414* | Lemma for the Axiom of Replacement with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.) |
Theorem | axrepndlem2 9415 | Lemma for the Axiom of Replacement with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
Theorem | axrepnd 9416 | A version of the Axiom of Replacement with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.) |
Theorem | axunndlem1 9417* | Lemma for the Axiom of Union with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.) |
Theorem | axunnd 9418 | A version of the Axiom of Union with no distinct variable conditions. (Contributed by NM, 2-Jan-2002.) |
Theorem | axpowndlem1 9419 | Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.) |
Theorem | axpowndlem2 9420* | Lemma for the Axiom of Power Sets with no distinct variable conditions. Revised to remove a redundant antecedent from the consequence. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (Revised and shortened by Wolf Lammen, 9-Jun-2019.) |
Theorem | axpowndlem3 9421* | Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.) (Revised by Mario Carneiro, 10-Dec-2016.) (Proof shortened by Wolf Lammen, 10-Jun-2019.) |
Theorem | axpowndlem4 9422 | 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 9423 | A version of the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002.) |
Theorem | axregndlem1 9424 | Lemma for the Axiom of Regularity with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) |
Theorem | axregndlem2 9425* | 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 9426 | 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 9427* | Lemma for the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.) |
Theorem | axinfnd 9428 | A version of the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002.) |
Theorem | axacndlem1 9429 | Lemma for the Axiom of Choice with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) |
Theorem | axacndlem2 9430 | Lemma for the Axiom of Choice with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) |
Theorem | axacndlem3 9431 | Lemma for the Axiom of Choice with no distinct variable conditions. (Contributed by NM, 3-Jan-2002.) |
Theorem | axacndlem4 9432* | 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 9433* | 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 9434 | 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 9435* | Axiom of Extensionality ax-ext 2602, reproved from conditionless ZFC version and predicate calculus. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
Theorem | zfcndrep 9436* | Axiom of Replacement ax-rep 4771, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
Theorem | zfcndun 9437* | Axiom of Union ax-un 6949, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
Theorem | zfcndpow 9438* | Axiom of Power Sets ax-pow 4843, reproved from conditionless ZFC axioms. The proof uses the "Axiom of Twoness," dtru 4857. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
Theorem | zfcndreg 9439* | Axiom of Regularity ax-reg 8497, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (Proof modification is discouraged.) |
Theorem | zfcndinf 9440* | Axiom of Infinity ax-inf 8535, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing theorem el 4847 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.) |
Theorem | zfcndac 9441* | Axiom of Choice ax-ac 9281, reproved from conditionless ZFC axioms. (Contributed by NM, 15-Aug-2003.) (New usage is discouraged.) (Proof modification is discouraged.) |
Syntax | cgch 9442 | Extend class notation to include the collection of sets that satisfy the GCH. |
GCH | ||
Definition | df-gch 9443* | 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 . 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 | ||
Theorem | elgch 9444* | Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH | ||
Theorem | fingch 9445 | A finite set is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH | ||
Theorem | gchi 9446 | 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 | ||
Theorem | gchen1 9447 | If , and is an infinite GCH-set, then in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH | ||
Theorem | gchen2 9448 | If , and is an infinite GCH-set, then in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH | ||
Theorem | gchor 9449 | If , and is an infinite GCH-set, then either or in cardinality. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH | ||
Theorem | engch 9450 | The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH GCH | ||
Theorem | gchdomtri 9451 | Under certain conditions, a GCH-set can demonstrate trichotomy of dominance. Lemma for gchac 9503. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH | ||
Theorem | fpwwe2cbv 9452* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 3-Jun-2015.) |
Theorem | fpwwe2lem1 9453* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 15-May-2015.) |
Theorem | fpwwe2lem2 9454* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 19-May-2015.) |
Theorem | fpwwe2lem3 9455* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 19-May-2015.) |
Theorem | fpwwe2lem5 9456* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 15-May-2015.) |
Theorem | fpwwe2lem6 9457* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 18-May-2015.) |
OrdIso OrdIso | ||
Theorem | fpwwe2lem7 9458* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 18-May-2015.) |
OrdIso OrdIso | ||
Theorem | fpwwe2lem8 9459* | Lemma for fpwwe2 9465. Show by induction that the two isometries and agree on their common domain. (Contributed by Mario Carneiro, 15-May-2015.) |
OrdIso OrdIso | ||
Theorem | fpwwe2lem9 9460* | Lemma for fpwwe2 9465. 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.) |
OrdIso OrdIso | ||
Theorem | fpwwe2lem10 9461* | Lemma for fpwwe2 9465. Given two well-orders and of parts of , one is an initial segment of the other. (Contributed by Mario Carneiro, 15-May-2015.) |
Theorem | fpwwe2lem11 9462* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 15-May-2015.) |
Theorem | fpwwe2lem12 9463* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 18-May-2015.) |
Theorem | fpwwe2lem13 9464* | Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 18-May-2015.) |
Theorem | fpwwe2 9465* | 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 8853. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) |
Theorem | fpwwecbv 9466* | Lemma for fpwwe 9468. (Contributed by Mario Carneiro, 15-May-2015.) |
Theorem | fpwwelem 9467* | Lemma for fpwwe 9468. (Contributed by Mario Carneiro, 15-May-2015.) |
Theorem | fpwwe 9468* | Given any function from the powerset of to , canth2 8113 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 8853. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.) |
Theorem | canth4 9469* | An "effective" form of Cantor's theorem canth 6608. 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.) |
Theorem | canthnumlem 9470* | Lemma for canthnum 9471. (Contributed by Mario Carneiro, 19-May-2015.) |
Theorem | canthnum 9471 | The set of well-orderable subsets of a set strictly dominates . A stronger form of canth2 8113. Corollary 1.4(a) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 19-May-2015.) |
Theorem | canthwelem 9472* | Lemma for canthwe 9473. (Contributed by Mario Carneiro, 31-May-2015.) |
Theorem | canthwe 9473* | The set of well-orders of a set strictly dominates . A stronger form of canth2 8113. Corollary 1.4(b) of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 31-May-2015.) |
Theorem | canthp1lem1 9474 | Lemma for canthp1 9476. (Contributed by Mario Carneiro, 18-May-2015.) |
Theorem | canthp1lem2 9475* | Lemma for canthp1 9476. (Contributed by Mario Carneiro, 18-May-2015.) |
Theorem | canthp1 9476 | A slightly stronger form of Cantor's theorem: For , . Corollary 1.6 of [KanamoriPincus] p. 417. (Contributed by Mario Carneiro, 18-May-2015.) |
Theorem | finngch 9477 | The exclusion of finite sets from consideration in df-gch 9443 is necessary, because otherwise finite sets larger than a singleton would violate the GCH property. (Contributed by Mario Carneiro, 10-Jun-2015.) |
Theorem | gchcda1 9478 | An infinite GCH-set is idempotent under cardinal successor. (Contributed by Mario Carneiro, 18-May-2015.) |
GCH | ||
Theorem | gchinf 9479 | An infinite GCH-set is Dedekind-infinite. (Contributed by Mario Carneiro, 31-May-2015.) |
GCH | ||
Theorem | pwfseqlem1 9480* | Lemma for pwfseq 9486. Derive a contradiction by diagonalization. (Contributed by Mario Carneiro, 31-May-2015.) |
Theorem | pwfseqlem2 9481* | Lemma for pwfseq 9486. (Contributed by Mario Carneiro, 18-Nov-2014.) (Revised by AV, 18-Sep-2021.) |
Theorem | pwfseqlem3 9482* | Lemma for pwfseq 9486. Using the construction from pwfseqlem1 9480, produce a function that maps any well-ordered infinite set to an element outside the set. (Contributed by Mario Carneiro, 31-May-2015.) |
Theorem | pwfseqlem4a 9483* | Lemma for pwfseqlem4 9484. (Contributed by Mario Carneiro, 7-Jun-2016.) |
Theorem | pwfseqlem4 9484* | Lemma for pwfseq 9486. Derive a final contradiction from the function in pwfseqlem3 9482. Applying fpwwe2 9465 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.) |
Theorem | pwfseqlem5 9485* |
Lemma for pwfseq 9486. Although in some ways pwfseqlem4 9484 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 8850. 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 8837. 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 8603), which can be used to construct a pairing function explicitly using properties of the ordinal exponential (infxpenc 8841). (Contributed by Mario Carneiro, 31-May-2015.) |
har OrdIso seq𝜔 | ||
Theorem | pwfseq 9486* | 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 9487 | 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 9488 | 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 9489 | 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 9490 | 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 | ||
Theorem | gchxpidm 9491 | 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 | ||
Theorem | gchpwdom 9492 | 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 9493 | If is a GCH-set and its powerset is well-orderable, then the successor aleph is equinumerous to the powerset of . (Contributed by Mario Carneiro, 15-May-2015.) |
GCH | ||
Theorem | gchaleph2 9494 | If and are GCH-sets, then the successor aleph is equinumerous to the powerset of . (Contributed by Mario Carneiro, 31-May-2015.) |
GCH GCH | ||
Theorem | hargch 9495 | If , then is a GCH-set. The much simpler converse to gchhar 9501. (Contributed by Mario Carneiro, 2-Jun-2015.) |
har GCH | ||
Theorem | alephgch 9496 | If is equinumerous to the powerset of , then is a GCH-set. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH | ||
Theorem | gch2 9497 | 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 GCH | ||
Theorem | gch3 9498 | An equivalent formulation of the generalized continuum hypothesis. (Contributed by Mario Carneiro, 15-May-2015.) |
GCH | ||
Theorem | gch-kn 9499* | 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 9403 to the successor aleph using enen2 8101. (Contributed by NM, 1-Oct-2004.) |
Theorem | gchaclem 9500 | Lemma for gchac 9503 (obsolete, used in Sierpiński's proof). (Contributed by Mario Carneiro, 15-May-2015.) |
GCH |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |