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 ∈ NC ∧ 1c <c Nc ( Spac ‘M)) → (M ↑c 0c) ∈ NC )
Theorem	nchoicelem16 6302*	Lemma for nchoice 6306. Set up stratification for nchoicelem17 6303. (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 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 ∈ 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 6304	Lemma for nchoice 6306. Set up stratification for nchoicelem19 6305. (Contributed by SF, 20-Mar-2015.)
⊢ {x ∣ ( Spac ‘x) ∈ Fin } ∈ 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 → ∃m ∈ NC (( Spac ‘m) ∈ 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 ∈ V ↦ (x +c 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 ∈ V → F ∈ V)
Theorem	frecex 6311	The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
⊢ F = FRec (G, I)    &   ⊢ G ∈ V    ⇒   ⊢ F ∈ V
Theorem	frecxp 6312	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 6313	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 6314	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 6315*	Lemma for fnfrec 6318. Establish stratification for induction. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (F ∈ V → {w ∣ ∀y∀z((wFy ∧ wFz) → y = z)} ∈ 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)    &   ⊢ (φ → G ∈ V)    &   ⊢ (φ → I ∈ dom G)    &   ⊢ (φ → ran G ⊆ dom G)    ⇒   ⊢ (φ → (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)    &   ⊢ (φ → G ∈ V)    &   ⊢ (φ → I ∈ dom G)    &   ⊢ (φ → ran G ⊆ dom G)    &   ⊢ (φ → X ∈ Nn )    &   ⊢ (φ → (X +c 1c)FY)    ⇒   ⊢ (φ → ∃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)    &   ⊢ (φ → G ∈ Funs )    &   ⊢ (φ → I ∈ dom G)    &   ⊢ (φ → ran G ⊆ dom G)    ⇒   ⊢ (φ → 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)    &   ⊢ (φ → G ∈ Funs )    &   ⊢ (φ → I ∈ dom G)    &   ⊢ (φ → ran G ⊆ dom G)    ⇒   ⊢ (φ → (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)    &   ⊢ (φ → 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 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~<℘A holds for these sets. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ Can = {x ∣ ℘1x ≈ 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 ℘1x. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ SCan = {x ∣ (y ∈ x ↦ {y}) ∈ V}
Theorem	dmsnfn 6325*	The domain of the singleton function. (Contributed by Scott Fenton, 20-Apr-2021.)
⊢ dom (x ∈ A ↦ {x}) = A
Theorem	epelcres 6326	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 6327	Membership in the class of Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (A ∈ Can ↔ ℘1A ≈ A)
Theorem	elscan 6328*	Membership in the class of strongly Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (A ∈ SCan ↔ (x ∈ A ↦ {x}) ∈ V)
Theorem	scancan 6329	Strongly Cantorian implies Cantorian. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (A ∈ SCan → A ∈ Can )

< Previous  Wrap >