P. 64 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 6301-6337   *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

< Previous  Wrap >