P. 64 of Theorem List - New Foundations Explorer

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

Type	Label	Description
Statement
Theorem	nchoicelem15 6301	Lemma for nchoice 6306. 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 6302*	Lemma for nchoice 6306. Set up stratification for nchoicelem17 6303. (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 6303	Lemma for nchoice 6306. 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 6304	Lemma for nchoice 6306. Set up stratification for nchoicelem19 6305. (Contributed by SF, 20-Mar-2015.)
|- {x | ( Spac ` x) e. Fin } e. _V
Theorem	nchoicelem19 6305	Lemma for nchoice 6306. 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 6306	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 6307	Extend the definition of a class to include the finite recursive function generator.
class FRec (F, I)
Definition	df-frec 6308*	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 6309	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 6310	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 6311	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 6312	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 6313	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 6314	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 6315*	Lemma for fnfrec 6318. 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 6316	Lemma for fnfrec 6318. 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 6317*	Lemma for fnfrec 6318. 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 6318	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 6319	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 6320	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 6321	Extend the definition of class to include the class of all Cantorian sets.
class Can
Definition	df-can 6322	Define the class of all Cantorian sets. These are so-called because Cantor's Theorem A~<~PA holds for these sets. (Contributed by Scott Fenton, 19-Apr-2021.)
|- Can = {x | ~P1 x ~~ x}
Syntax	cscan 6323	Extend the definition of class to include the class of all strongly Cantorian sets.
class SCan
Definition	df-scan 6324*	Define the class of strongly Cantorian sets. Unline general Cantorian sets, this fixes a specific mapping between x and ~P1 x. (Contributed by Scott Fenton, 19-Apr-2021.)
|- SCan = {x | (y e. x |-> {y}) e. _V}
Theorem	dmsnfn 6325*	The domain of the singleton function. (Contributed by Scott Fenton, 20-Apr-2021.)
|- dom (x e. A |-> {x}) = A
Theorem	epelcres 6326	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 6327	Membership in the class of Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (A e. Can <-> ~P1 A ~~ A)
Theorem	elscan 6328*	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 6329	Strongly Cantorian implies Cantorian. (Contributed by Scott Fenton, 19-Apr-2021.)
|- (A e. SCan -> A e. Can )

< Previous  Wrap >