P. 64 of Theorem List - New Foundations Explorer

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

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.)
|- (M e. NC -> 1c <_c Nc ( Spac ` M))
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.)
|- ((M e. NC /\ Nc ( Spac ` M) = 1c) -> -. (M ↑c 0c) e. 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.)
|- ((M e. NC /\ 1c <c Nc ( Spac ` M)) -> (M ↑c 0c) e. NC )
Theorem	nchoicelem16 6304*	Lemma for nchoice 6308. Set up stratification for nchoicelem17 6305. (Contributed by SF, 19-Mar-2015.)
|- {t | ( <_c We NC -> A.m e. NC ( Nc ( Spac ` m) = (1c +o t) -> (( Spac ` Tc m) e. Fin /\ ( Nc ( Spac ` Tc m) = ( Tc Nc ( Spac ` m) +o 1c) \/ Nc ( Spac ` Tc m) = ( Tc Nc ( Spac ` m) +o 2c)))))} e. _V
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 /\ M e. NC /\ ( Spac ` M) e. Fin ) -> (( Spac ` Tc M) e. Fin /\ ( Nc ( Spac ` Tc M) = ( Tc Nc ( Spac ` M) +o 1c) \/ Nc ( Spac ` Tc M) = ( Tc Nc ( Spac ` M) +o 2c))))
Theorem	nchoicelem18 6306	Lemma for nchoice 6308. Set up stratification for nchoicelem19 6307. (Contributed by SF, 20-Mar-2015.)
|- {x | ( Spac ` x) e. Fin } e. _V
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 -> E.m e. NC (( Spac ` m) e. Fin /\ Tc m = m))
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
2.4.7  Finite recursion
Syntax	cfrec 6309	Extend the definition of a class to include the finite recursive function generator.
class FRec (F, I)
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 (F, I) = Clos1 ({<.0c, I>.}, PProd ((x e. _V |-> (x +o 1c)), F))
Theorem	freceq12 6311	Equality theorem for finite recursive function generator. (Contributed by Scott Fenton, 31-Jul-2019.)
|- ((F = G /\ I = J) -> FRec (F, I) = FRec (G, J))
Theorem	frecexg 6312	The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
|- F = FRec (G, I)   =>   |- (G e. V -> F e. _V)
Theorem	frecex 6313	The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
|- F = FRec (G, I)   &   |- G e. _V   =>   |- F e. _V
Theorem	frecxp 6314	Subset relationship for the finite recursive function generator. (Contributed by Scott Fenton, 30-Jul-2019.)
|- F = FRec (G, I)   &   |- G e. _V   =>   |- F C_ ( Nn X. (ran G u. {I}))
Theorem	frecxpg 6315	Subset relationship for the finite recursive function generator. (Contributed by Scott Fenton, 31-Jul-2019.)
|- F = FRec (G, I)   =>   |- (G e. V -> F C_ ( Nn X. (ran G u. {I})))
Theorem	dmfrec 6316	The domain of the finite recursive function generator is the naturals. (Contributed by Scott Fenton, 31-Jul-2019.)
|- F = FRec (G, I)   &   |- (ph -> G e. V)   &   |- (ph -> I e. dom G)   &   |- (ph -> ran G C_ dom G)   =>   |- (ph -> dom F = Nn )
Theorem	fnfreclem1 6317*	Lemma for fnfrec 6320. Establish stratification for induction. (Contributed by Scott Fenton, 31-Jul-2019.)
|- (F e. V -> {w | A.yA.z((wFy /\ wFz) -> y = z)} e. _V)
Theorem	fnfreclem2 6318	Lemma for fnfrec 6320. Calculate the unique value of F at zero. (Contributed by Scott Fenton, 31-Jul-2019.)
|- F = FRec (G, I)   &   |- (ph -> G e. V)   &   |- (ph -> I e. dom G)   &   |- (ph -> ran G C_ dom G)   =>   |- (ph -> (0cFX -> X = I))
Theorem	fnfreclem3 6319*	Lemma for fnfrec 6320. The value of F at a successor is G related to a previous element. (Contributed by Scott Fenton, 31-Jul-2019.)
|- F = FRec (G, I)   &   |- (ph -> G e. V)   &   |- (ph -> I e. dom G)   &   |- (ph -> ran G C_ dom G)   &   |- (ph -> X e. Nn )   &   |- (ph -> (X +o 1c)FY)   =>   |- (ph -> E.z(XFz /\ zGY))
Theorem	fnfrec 6320	The recursive function generator is a function over the finite cardinals. (Contributed by Scott Fenton, 31-Jul-2019.)
|- F = FRec (G, I)   &   |- (ph -> G e. Funs )   &   |- (ph -> I e. dom G)   &   |- (ph -> ran G C_ dom G)   =>   |- (ph -> F Fn Nn )
Theorem	frec0 6321	Calculate the value of the finite recursive function generator at zero. (Contributed by Scott Fenton, 31-Jul-2019.)
|- F = FRec (G, I)   &   |- (ph -> G e. Funs )   &   |- (ph -> I e. dom G)   &   |- (ph -> ran G C_ dom G)   =>   |- (ph -> (F` 0c) = I)
Theorem	frecsuc 6322	Calculate the value of the finite recursive function generator at a successor. (Contributed by Scott Fenton, 31-Jul-2019.)
|- F = FRec (G, I)   &   |- (ph -> G e. Funs )   &   |- (ph -> I e. dom G)   &   |- (ph -> ran G C_ dom G)   &   |- (ph -> X e. Nn )   =>   |- (ph -> (F` (X +o 1c)) = (G` (F` X)))
2.5  Cantorian and Strongly Cantorian Sets
Syntax	ccan 6323	Extend the definition of class to include the class of all Cantorian sets.
class Can
Definition	df-can 6324	Define the class of all Cantorian sets. These are so-called because Cantor's Theorem Nc A <c Nc ~PA holds for these sets. Definition from [Rosser] p. 347 and [Holmes] p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
|- Can = {x | ~P1 x ~~ x}
Syntax	cscan 6325	Extend the definition of class to include the class of all strongly Cantorian sets.
class SCan
Definition	df-scan 6326*	Define the class of strongly Cantorian sets. Unlike general Cantorian sets, this fixes a specific mapping between x and ~P1 x. Definition from [Holmes] p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
|- SCan = {x | (y e. x |-> {y}) e. _V}
Theorem	dmsnfn 6327*	The domain of the singleton function. (Contributed by Scott Fenton, 20-Apr-2021.)
|- dom (x e. A |-> {x}) = A
Theorem	epelcres 6328	Version of epelc 4765 with a restriction in place. (Contributed by Scott Fenton, 20-Apr-2021.)
|- Y e. _V   =>   |- (X e. A -> (X( _E |` A)Y <-> X e. Y))
Theorem	elcan 6329	Membership in the class of Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (A e. Can <-> ~P1 A ~~ A)
Theorem	elscan 6330*	Membership in the class of strongly Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (A e. SCan <-> (x e. A |-> {x}) e. _V)
Theorem	scancan 6331	Strongly Cantorian implies Cantorian. Observation from [Holmes], p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (A e. SCan -> A e. 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.)
|- (A e. V -> (A e. Can <-> Nc ~P1 A = Nc A))
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.)
|- (A e. Can -> Nc ~P1 A = Nc A)
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.)
|- (A e. Can -> Nc A <c Nc ~PA)
Theorem	cantcb 6335	The cardinality of a Cantorian set is equal to the Tc raising of that cardinal. (Contributed by Scott Fenton, 23-Apr-2021.)
|- (A e. V -> (A e. Can <-> Tc Nc A = Nc A))
Theorem	cantc 6336	The cardinality of a Cantorian set is equal to the Tc raising of that cardinal. (Contributed by Scott Fenton, 22-Apr-2021.)
|- (A e. Can -> Tc Nc A = Nc A)
Theorem	vncan 6337	The universe is not Cantorian. Theorem XI.1.8 of [Rosser] p. 348. (Contributed by Scott Fenton, 22-Apr-2021.)
|- -. _V e. 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.
Theorem	conventions 6338	Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (MPE, set.mm). Community. The Metamath mailing list also covers New Foundations set theory and is at: https://groups.google.com/g/metamath. (Contributed by the Metamath team, 20-Jan-2024.) (New usage is discouraged.)
|- ph   =>   |- ph

< Previous  Wrap >