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.)
|
NC 1c
c Nc Spac
↑c
0c
NC |
|
Theorem | nchoicelem16 6302* |
Lemma for nchoice 6306. Set up stratification for nchoicelem17 6303.
(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 |
|
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 NC Spac Fin Spac Tc
Fin Nc Spac
Tc
Tc Nc Spac
1c
Nc Spac Tc
Tc Nc Spac
2c |
|
Theorem | nchoicelem18 6304 |
Lemma for nchoice 6306. Set up stratification for nchoicelem19 6305.
(Contributed by SF, 20-Mar-2015.)
|
Spac Fin |
|
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 NC Spac
Fin Tc
|
|
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.
|
FRec |
|
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 Clos1 0c PProd
1c |
|
Theorem | freceq12 6309 |
Equality theorem for finite recursive function generator. (Contributed
by Scott Fenton, 31-Jul-2019.)
|
FRec FRec |
|
Theorem | frecexg 6310 |
The finite recursive function generator preserves sethood. (Contributed
by Scott Fenton, 30-Jul-2019.)
|
FRec
|
|
Theorem | frecex 6311 |
The finite recursive function generator preserves sethood. (Contributed
by Scott Fenton, 30-Jul-2019.)
|
FRec |
|
Theorem | frecxp 6312 |
Subset relationship for the finite recursive function generator.
(Contributed by Scott Fenton, 30-Jul-2019.)
|
FRec Nn |
|
Theorem | frecxpg 6313 |
Subset relationship for the finite recursive function generator.
(Contributed by Scott Fenton, 31-Jul-2019.)
|
FRec
Nn |
|
Theorem | dmfrec 6314 |
The domain of the finite recursive function generator is the naturals.
(Contributed by Scott Fenton, 31-Jul-2019.)
|
FRec Nn |
|
Theorem | fnfreclem1 6315* |
Lemma for fnfrec 6318. Establish stratification for induction.
(Contributed by Scott Fenton, 31-Jul-2019.)
|
|
|
Theorem | fnfreclem2 6316 |
Lemma for fnfrec 6318. Calculate the unique value of at zero.
(Contributed by Scott Fenton, 31-Jul-2019.)
|
FRec 0c |
|
Theorem | fnfreclem3 6317* |
Lemma for fnfrec 6318. The value of at a successor is related
to a previous element. (Contributed by Scott Fenton, 31-Jul-2019.)
|
FRec Nn
1c |
|
Theorem | fnfrec 6318 |
The recursive function generator is a function over the finite
cardinals. (Contributed by Scott Fenton, 31-Jul-2019.)
|
FRec Funs
Nn |
|
Theorem | frec0 6319 |
Calculate the value of the finite recursive function generator at zero.
(Contributed by Scott Fenton, 31-Jul-2019.)
|
FRec Funs
0c |
|
Theorem | frecsuc 6320 |
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
|
|
Syntax | ccan 6321 |
Extend the definition of class to include the class of all Cantorian
sets.
|
Can |
|
Definition | df-can 6322 |
Define the class of all Cantorian sets. These are so-called because
Cantor's Theorem ~< holds for these sets.
(Contributed by
Scott Fenton, 19-Apr-2021.)
|
Can 1 |
|
Syntax | cscan 6323 |
Extend the definition of class to include the class of all strongly
Cantorian sets.
|
SCan |
|
Definition | df-scan 6324* |
Define the class of strongly Cantorian sets. Unline general Cantorian
sets, this fixes a specific mapping between and 1 .
(Contributed by Scott Fenton, 19-Apr-2021.)
|
SCan
|
|
Theorem | dmsnfn 6325* |
The domain of the singleton function. (Contributed by Scott Fenton,
20-Apr-2021.)
|
|
|
Theorem | epelcres 6326 |
Version of epelc 4765 with a restriction in place. (Contributed by
Scott Fenton, 20-Apr-2021.)
|
|
|
Theorem | elcan 6327 |
Membership in the class of Cantorian sets. (Contributed by Scott
Fenton, 19-Apr-2021.)
|
Can 1 |
|
Theorem | elscan 6328* |
Membership in the class of strongly Cantorian sets. (Contributed by
Scott Fenton, 19-Apr-2021.)
|
SCan |
|
Theorem | scancan 6329 |
Strongly Cantorian implies Cantorian. (Contributed by Scott Fenton,
19-Apr-2021.)
|
SCan Can |