Home New Foundations ExplorerTheorem 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

Theorem List for New Foundations Explorer - 6301-6338   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremnchoicelem13 6301 Lemma for nchoice 6308. The cardinality of a special set is at least one. (Contributed by SF, 18-Mar-2015.)
NC 1c c Nc Spac

Theoremnchoicelem14 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 Spac 1c c 0c NC

Theoremnchoicelem15 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 1c c Nc Spac c 0c NC

Theoremnchoicelem16 6304* Lemma for nchoice 6308. Set up stratification for nchoicelem17 6305. (Contributed by SF, 19-Mar-2015.)
c We NC NC Nc Spac 1c Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c

Theoremnchoicelem17 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 Spac Fin Spac Tc Fin Nc Spac Tc Tc Nc Spac 1c Nc Spac Tc Tc Nc Spac 2c

Theoremnchoicelem18 6306 Lemma for nchoice 6308. Set up stratification for nchoicelem19 6307. (Contributed by SF, 20-Mar-2015.)
Spac Fin

Theoremnchoicelem19 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 Spac Fin Tc

Theoremnchoice 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

2.4.7  Finite recursion

Syntaxcfrec 6309 Extend the definition of a class to include the finite recursive function generator.
FRec

Definitiondf-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 0c PProd 1c

Theoremfreceq12 6311 Equality theorem for finite recursive function generator. (Contributed by Scott Fenton, 31-Jul-2019.)
FRec FRec

Theoremfrecexg 6312 The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
FRec

Theoremfrecex 6313 The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
FRec

Theoremfrecxp 6314 Subset relationship for the finite recursive function generator. (Contributed by Scott Fenton, 30-Jul-2019.)
FRec               Nn

Theoremfrecxpg 6315 Subset relationship for the finite recursive function generator. (Contributed by Scott Fenton, 31-Jul-2019.)
FRec        Nn

Theoremdmfrec 6316 The domain of the finite recursive function generator is the naturals. (Contributed by Scott Fenton, 31-Jul-2019.)
FRec                             Nn

Theoremfnfreclem1 6317* Lemma for fnfrec 6320. Establish stratification for induction. (Contributed by Scott Fenton, 31-Jul-2019.)

Theoremfnfreclem2 6318 Lemma for fnfrec 6320. Calculate the unique value of at zero. (Contributed by Scott Fenton, 31-Jul-2019.)
FRec                             0c

Theoremfnfreclem3 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        1c

Theoremfnfrec 6320 The recursive function generator is a function over the finite cardinals. (Contributed by Scott Fenton, 31-Jul-2019.)
FRec        Funs                      Nn

Theoremfrec0 6321 Calculate the value of the finite recursive function generator at zero. (Contributed by Scott Fenton, 31-Jul-2019.)
FRec        Funs                      0c

Theoremfrecsuc 6322 Calculate the value of the finite recursive function generator at a successor. (Contributed by Scott Fenton, 31-Jul-2019.)
FRec        Funs                      Nn        1c

2.5  Cantorian and Strongly Cantorian Sets

Syntaxccan 6323 Extend the definition of class to include the class of all Cantorian sets.
Can

Definitiondf-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

Syntaxcscan 6325 Extend the definition of class to include the class of all strongly Cantorian sets.
SCan

Definitiondf-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

Theoremdmsnfn 6327* The domain of the singleton function. (Contributed by Scott Fenton, 20-Apr-2021.)

Theoremepelcres 6328 Version of epelc 4765 with a restriction in place. (Contributed by Scott Fenton, 20-Apr-2021.)

Theoremelcan 6329 Membership in the class of Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
Can 1

Theoremelscan 6330* Membership in the class of strongly Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
SCan

Theoremscancan 6331 Strongly Cantorian implies Cantorian. Observation from [Holmes], p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
SCan Can

Theoremcanncb 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

Theoremcannc 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

Theoremcanltpw 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

Theoremcantcb 6335 The cardinality of a Cantorian set is equal to the Tc raising of that cardinal. (Contributed by Scott Fenton, 23-Apr-2021.)
Can Tc Nc Nc

Theoremcantc 6336 The cardinality of a Cantorian set is equal to the Tc raising of that cardinal. (Contributed by Scott Fenton, 22-Apr-2021.)
Can Tc Nc Nc

Theoremvncan 6337 The universe is not Cantorian. Theorem XI.1.8 of [Rosser] p. 348. (Contributed by Scott Fenton, 22-Apr-2021.)
Can

PART 3  GUIDES AND MISCELLANEA

3.1  Guides (conventions, explanations, and examples)

3.1.1  Conventions

This section describes the conventions we use. These conventions often refer to existing mathematical practices, which are discussed in more detail in other references.

Theoremconventions 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.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6338
 Copyright terms: Public domain < Previous  Wrap >