P. 64 of Theorem List - New Foundations Explorer

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

Type	Label	Description
Statement
Theorem	nchoicelem12 6301	Lemma for nchoice 6309. If the T-raising of a cardinal yields a finite special set, then so does the initial set. Theorem 7.1 of [Specker] p. 974. (Contributed by SF, 18-Mar-2015.)
⊢ ((M ∈ NC ∧ ( Spac ‘ Tc M) ∈ Fin ) → ( Spac ‘M) ∈ Fin )
Theorem	nchoicelem13 6302	Lemma for nchoice 6309. 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 6303	Lemma for nchoice 6309. 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 6304	Lemma for nchoice 6309. 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 6305*	Lemma for nchoice 6309. Set up stratification for nchoicelem17 6306. (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 6306	Lemma for nchoice 6309. 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 6307	Lemma for nchoice 6309. Set up stratification for nchoicelem19 6308. (Contributed by SF, 20-Mar-2015.)
⊢ {x ∣ ( Spac ‘x) ∈ Fin } ∈ V
Theorem	nchoicelem19 6308	Lemma for nchoice 6309. 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 6309	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 6310	Extend the definition of a class to include the finite recursive function generator.
class FRec (F, I)
Definition	df-frec 6311*	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 6312	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 6313	The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
⊢ F = FRec (G, I)    ⇒   ⊢ (G ∈ V → F ∈ V)
Theorem	frecex 6314	The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
⊢ F = FRec (G, I)    &   ⊢ G ∈ V    ⇒   ⊢ F ∈ V
Theorem	frecxp 6315	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 6316	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 6317	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 6318*	Lemma for fnfrec 6321. Establish stratification for induction. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (F ∈ V → {w ∣ ∀y∀z((wFy ∧ wFz) → y = z)} ∈ V)
Theorem	fnfreclem2 6319	Lemma for fnfrec 6321. 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 6320*	Lemma for fnfrec 6321. 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 6321	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 6322	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 6323	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 6324	Extend the definition of class to include the class of all Cantorian sets.
class Can
Definition	df-can 6325	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 6326	Extend the definition of class to include the class of all strongly Cantorian sets.
class SCan
Definition	df-scan 6327*	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 6328*	The domain of the singleton function. (Contributed by Scott Fenton, 20-Apr-2021.)
⊢ dom (x ∈ A ↦ {x}) = A
Theorem	epelcres 6329	Version of epelc 4766 with a restriction in place. (Contributed by Scott Fenton, 20-Apr-2021.)
⊢ Y ∈ V    ⇒   ⊢ (X ∈ A → (X( E ↾ A)Y ↔ X ∈ Y))
Theorem	elcan 6330	Membership in the class of Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (A ∈ Can ↔ ℘1A ≈ A)
Theorem	elscan 6331*	Membership in the class of strongly Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (A ∈ SCan ↔ (x ∈ A ↦ {x}) ∈ V)
Theorem	scancan 6332	Strongly Cantorian implies Cantorian. Observation from [Holmes], p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
⊢ (A ∈ SCan → A ∈ Can )
Theorem	canncb 6333	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 6334	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 6335	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 6336	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 6337	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 6338	The universe is not Cantorian. Theorem XI.1.8 of [Rosser] p. 348. (Contributed by Scott Fenton, 22-Apr-2021.)
⊢ ¬ V ∈ Can
PART 3  GUIDES AND MISCELLANEA
3.1  Guides (conventions, explanations, and examples)
3.1.1  Conventions This section describes the conventions we use. These conventions often refer to existing mathematical practices, which are discussed in more detail in other references.
Theorem	conventions 6339	Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (MPE, set.mm). Community. The Metamath mailing list also covers New Foundations set theory and is at: https://groups.google.com/g/metamath. (Contributed by the Metamath team, 20-Jan-2024.) (New usage is discouraged.)
⊢ φ    ⇒   ⊢ φ

< Previous  Wrap >