Home | New
Foundations Explorer Theorem List (p. 64 of 64) | < Previous Wrap > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > NFE Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nchoicelem13 6301 | Lemma for nchoice 6308. The cardinality of a special set is at least one. (Contributed by SF, 18-Mar-2015.) |
NC 1_{c} _{c} Nc Sp_{ac} | ||
Theorem | nchoicelem14 6302 | Lemma for nchoice 6308. When the special set generator yields a singleton, then the cardinal is not raisable. (Contributed by SF, 19-Mar-2015.) |
NC Nc Sp_{ac} 1_{c} ↑_{c} 0_{c} NC | ||
Theorem | nchoicelem15 6303 | Lemma for nchoice 6308. When the special set generator does not yield a singleton, then the cardinal is raisable. (Contributed by SF, 19-Mar-2015.) |
NC 1_{c} _{c} Nc Sp_{ac} ↑_{c} 0_{c} NC | ||
Theorem | nchoicelem16 6304* | Lemma for nchoice 6308. Set up stratification for nchoicelem17 6305. (Contributed by SF, 19-Mar-2015.) |
_{c} We NC NC Nc Sp_{ac} 1_{c} Sp_{ac} T_{c} Fin Nc Sp_{ac} T_{c} T_{c} Nc Sp_{ac} 1_{c} Nc Sp_{ac} T_{c} T_{c} Nc Sp_{ac} 2_{c} | ||
Theorem | nchoicelem17 6305 | Lemma for nchoice 6308. If the special set of a cardinal is finite, then so is the special set of its T-raising, and there is a calculable relationship between their sizes. Theorem 7.2 of [Specker] p. 974. (Contributed by SF, 19-Mar-2015.) |
_{c} We NC NC Sp_{ac} Fin Sp_{ac} T_{c} Fin Nc Sp_{ac} T_{c} T_{c} Nc Sp_{ac} 1_{c} Nc Sp_{ac} T_{c} T_{c} Nc Sp_{ac} 2_{c} | ||
Theorem | nchoicelem18 6306 | Lemma for nchoice 6308. Set up stratification for nchoicelem19 6307. (Contributed by SF, 20-Mar-2015.) |
Sp_{ac} Fin | ||
Theorem | nchoicelem19 6307 | Lemma for nchoice 6308. Assuming well-ordering, there is a cardinal with a finite special set that is its own T-raising. Theorem 7.3 of [Specker] p. 974. (Contributed by SF, 20-Mar-2015.) |
_{c} We NC NC Sp_{ac} Fin T_{c} | ||
Theorem | nchoice 6308 | Cardinal less than or equal does not well-order the cardinals. This is equivalent to saying that the axiom of choice from ZFC is false in NF. Theorem 7.5 of [Specker] p. 974. (Contributed by SF, 20-Mar-2015.) |
_{c} We NC | ||
Syntax | cfrec 6309 | Extend the definition of a class to include the finite recursive function generator. |
FRec | ||
Definition | df-frec 6310* | Define the finite recursive function generator. This is a function over Nn that obeys the standard recursion relationship. Definition adapted from theorem XI.3.24 of [Rosser] p. 412. (Contributed by Scott Fenton, 30-Jul-2019.) |
FRec Clos1 0_{c} PProd 1_{c} | ||
Theorem | freceq12 6311 | Equality theorem for finite recursive function generator. (Contributed by Scott Fenton, 31-Jul-2019.) |
FRec FRec | ||
Theorem | frecexg 6312 | The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.) |
FRec | ||
Theorem | frecex 6313 | The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.) |
FRec | ||
Theorem | frecxp 6314 | Subset relationship for the finite recursive function generator. (Contributed by Scott Fenton, 30-Jul-2019.) |
FRec Nn | ||
Theorem | frecxpg 6315 | Subset relationship for the finite recursive function generator. (Contributed by Scott Fenton, 31-Jul-2019.) |
FRec Nn | ||
Theorem | dmfrec 6316 | The domain of the finite recursive function generator is the naturals. (Contributed by Scott Fenton, 31-Jul-2019.) |
FRec Nn | ||
Theorem | fnfreclem1 6317* | Lemma for fnfrec 6320. Establish stratification for induction. (Contributed by Scott Fenton, 31-Jul-2019.) |
Theorem | fnfreclem2 6318 | Lemma for fnfrec 6320. Calculate the unique value of at zero. (Contributed by Scott Fenton, 31-Jul-2019.) |
FRec 0_{c} | ||
Theorem | fnfreclem3 6319* | Lemma for fnfrec 6320. The value of at a successor is related to a previous element. (Contributed by Scott Fenton, 31-Jul-2019.) |
FRec Nn 1_{c} | ||
Theorem | fnfrec 6320 | The recursive function generator is a function over the finite cardinals. (Contributed by Scott Fenton, 31-Jul-2019.) |
FRec Funs Nn | ||
Theorem | frec0 6321 | Calculate the value of the finite recursive function generator at zero. (Contributed by Scott Fenton, 31-Jul-2019.) |
FRec Funs 0_{c} | ||
Theorem | frecsuc 6322 | Calculate the value of the finite recursive function generator at a successor. (Contributed by Scott Fenton, 31-Jul-2019.) |
FRec Funs Nn 1_{c} | ||
Syntax | ccan 6323 | Extend the definition of class to include the class of all Cantorian sets. |
Can | ||
Definition | df-can 6324 | Define the class of all Cantorian sets. These are so-called because Cantor's Theorem Nc _{c} Nc holds for these sets. Definition from [Rosser] p. 347 and [Holmes] p. 134. (Contributed by Scott Fenton, 19-Apr-2021.) |
Can _{1} | ||
Syntax | cscan 6325 | Extend the definition of class to include the class of all strongly Cantorian sets. |
SCan | ||
Definition | df-scan 6326* | Define the class of strongly Cantorian sets. Unlike general Cantorian sets, this fixes a specific mapping between and _{1} . Definition from [Holmes] p. 134. (Contributed by Scott Fenton, 19-Apr-2021.) |
SCan | ||
Theorem | dmsnfn 6327* | The domain of the singleton function. (Contributed by Scott Fenton, 20-Apr-2021.) |
Theorem | epelcres 6328 | Version of epelc 4765 with a restriction in place. (Contributed by Scott Fenton, 20-Apr-2021.) |
Theorem | elcan 6329 | Membership in the class of Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.) |
Can _{1} | ||
Theorem | elscan 6330* | Membership in the class of strongly Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.) |
SCan | ||
Theorem | scancan 6331 | Strongly Cantorian implies Cantorian. Observation from [Holmes], p. 134. (Contributed by Scott Fenton, 19-Apr-2021.) |
SCan Can | ||
Theorem | canncb 6332 | The cardinality of a Cantorian set is equal to the cardinality of its unit power set. (Contributed by Scott Fenton, 23-Apr-2021.) |
Can Nc _{1} Nc | ||
Theorem | cannc 6333 | The cardinality of a Cantorian set is equal to the cardinality of its unit power set. (Contributed by Scott Fenton, 21-Apr-2021.) |
Can Nc _{1} Nc | ||
Theorem | canltpw 6334 | The cardinality of a Cantorian set is strictly less than the cardinality of its power set. (Contributed by Scott Fenton, 21-Apr-2021.) |
Can Nc _{c} Nc | ||
Theorem | cantcb 6335 | The cardinality of a Cantorian set is equal to the T_{c} raising of that cardinal. (Contributed by Scott Fenton, 23-Apr-2021.) |
Can T_{c} Nc Nc | ||
Theorem | cantc 6336 | The cardinality of a Cantorian set is equal to the T_{c} raising of that cardinal. (Contributed by Scott Fenton, 22-Apr-2021.) |
Can T_{c} Nc Nc | ||
Theorem | vncan 6337 | The universe is not Cantorian. Theorem XI.1.8 of [Rosser] p. 348. (Contributed by Scott Fenton, 22-Apr-2021.) |
Can | ||
This section describes the conventions we use. These conventions often refer to existing mathematical practices, which are discussed in more detail in other references. | ||
Theorem | conventions 6338 |
Unless there is a reason to diverge, we follow the conventions of the
Metamath Proof Explorer (MPE, set.mm).
(Contributed by the Metamath team, 20-Jan-2024.) (New usage is discouraged.) |
< Previous Wrap > |
Copyright terms: Public domain | < Previous Wrap > |