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 ∈ 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 ∈ NC ∧ Nc ( Spac ‘M) = 1c) → ¬ (M ↑c 0c)
∈ 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 ∈ NC ∧ 1c <c Nc ( Spac
‘M)) → (M ↑c 0c)
∈ NC
) |
|
Theorem | nchoicelem16 6304* |
Lemma for nchoice 6308. Set up stratification for nchoicelem17 6305.
(Contributed by SF, 19-Mar-2015.)
|
⊢ {t ∣ ( ≤c We NC → ∀m ∈ NC ( Nc ( Spac
‘m) = (1c
+c t) → (( Spac ‘ Tc m)
∈ Fin ∧ ( Nc ( Spac ‘ Tc m) =
( Tc Nc (
Spac ‘m) +c 1c) ∨ Nc ( Spac ‘ Tc m) =
( Tc Nc (
Spac ‘m) +c 2c)))))}
∈ 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 ∈ NC ∧ ( Spac
‘M) ∈ Fin ) → ((
Spac ‘ Tc M)
∈ Fin ∧ ( Nc ( Spac ‘ Tc M) =
( Tc Nc (
Spac ‘M) +c 1c) ∨ Nc ( Spac ‘ Tc M) =
( Tc Nc (
Spac ‘M) +c
2c)))) |
|
Theorem | nchoicelem18 6306 |
Lemma for nchoice 6308. Set up stratification for nchoicelem19 6307.
(Contributed by SF, 20-Mar-2015.)
|
⊢ {x ∣ ( Spac
‘x) ∈ Fin } ∈ 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 → ∃m ∈ NC (( Spac ‘m) ∈ 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 ∈ V ↦ (x +c 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 ∈ V →
F ∈
V) |
|
Theorem | frecex 6313 |
The finite recursive function generator preserves sethood. (Contributed
by Scott Fenton, 30-Jul-2019.)
|
⊢ F = FRec (G, I)
& ⊢ G ∈ V ⇒ ⊢ F ∈ V |
|
Theorem | frecxp 6314 |
Subset relationship for the finite recursive function generator.
(Contributed by Scott Fenton, 30-Jul-2019.)
|
⊢ F = FRec (G, I)
& ⊢ G ∈ V ⇒ ⊢ F ⊆ ( Nn × (ran
G ∪ {I})) |
|
Theorem | frecxpg 6315 |
Subset relationship for the finite recursive function generator.
(Contributed by Scott Fenton, 31-Jul-2019.)
|
⊢ F = FRec (G, I) ⇒ ⊢ (G ∈ V →
F ⊆ (
Nn × (ran G ∪ {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)
& ⊢ (φ
→ G ∈ V)
& ⊢ (φ
→ I ∈ dom G)
& ⊢ (φ
→ ran G ⊆ dom G) ⇒ ⊢ (φ
→ dom F = Nn ) |
|
Theorem | fnfreclem1 6317* |
Lemma for fnfrec 6320. Establish stratification for induction.
(Contributed by Scott Fenton, 31-Jul-2019.)
|
⊢ (F ∈ V →
{w ∣
∀y∀z((wFy ∧ wFz) →
y = z)} ∈
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)
& ⊢ (φ
→ G ∈ V)
& ⊢ (φ
→ I ∈ dom G)
& ⊢ (φ
→ ran G ⊆ dom G) ⇒ ⊢ (φ
→ (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)
& ⊢ (φ
→ G ∈ V)
& ⊢ (φ
→ I ∈ dom G)
& ⊢ (φ
→ ran G ⊆ dom G)
& ⊢ (φ
→ X ∈ Nn ) & ⊢ (φ
→ (X +c
1c)FY) ⇒ ⊢ (φ
→ ∃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)
& ⊢ (φ
→ G ∈ Funs ) & ⊢ (φ
→ I ∈ dom G)
& ⊢ (φ
→ ran G ⊆ dom G) ⇒ ⊢ (φ
→ 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)
& ⊢ (φ
→ G ∈ Funs ) & ⊢ (φ
→ I ∈ dom G)
& ⊢ (φ
→ ran G ⊆ dom G) ⇒ ⊢ (φ
→ (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)
& ⊢ (φ
→ G ∈ Funs ) & ⊢ (φ
→ I ∈ dom G)
& ⊢ (φ
→ ran G ⊆ dom G)
& ⊢ (φ
→ X ∈ Nn
) ⇒ ⊢ (φ
→ (F ‘(X +c 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
℘A holds for these sets. Definition
from [Rosser] p. 347 and [Holmes] p. 134. (Contributed by Scott Fenton,
19-Apr-2021.)
|
⊢ Can = {x ∣ ℘1x ≈ 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 ℘1x.
Definition from [Holmes] p. 134.
(Contributed by Scott Fenton,
19-Apr-2021.)
|
⊢ SCan = {x ∣ (y ∈ x ↦ {y}) ∈
V} |
|
Theorem | dmsnfn 6327* |
The domain of the singleton function. (Contributed by Scott Fenton,
20-Apr-2021.)
|
⊢ dom (x
∈ A
↦ {x})
= A |
|
Theorem | epelcres 6328 |
Version of epelc 4765 with a restriction in place. (Contributed by
Scott
Fenton, 20-Apr-2021.)
|
⊢ Y ∈ V ⇒ ⊢ (X ∈ A →
(X( E ↾
A)Y
↔ X ∈ Y)) |
|
Theorem | elcan 6329 |
Membership in the class of Cantorian sets. (Contributed by Scott
Fenton, 19-Apr-2021.)
|
⊢ (A ∈ Can ↔ ℘1A ≈ A) |
|
Theorem | elscan 6330* |
Membership in the class of strongly Cantorian sets. (Contributed by
Scott Fenton, 19-Apr-2021.)
|
⊢ (A ∈ SCan ↔
(x ∈
A ↦
{x}) ∈
V) |
|
Theorem | scancan 6331 |
Strongly Cantorian implies Cantorian. Observation from [Holmes],
p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
|
⊢ (A ∈ SCan →
A ∈
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 ∈ V →
(A ∈
Can ↔ Nc ℘1A = 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 ∈ Can → Nc ℘1A = 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 ∈ Can → Nc A
<c Nc ℘A) |
|
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 ∈ V →
(A ∈
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 ∈ 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 ∈
Can |