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 ∈ 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

< Previous  Wrap >