P. 63 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 6201-6300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	le0nc 6201	Cardinal zero is a minimal element of cardinal less than or equal. Lemma 1 of theorem XI.2.15 of [Rosser] p. 376. (Contributed by SF, 12-Mar-2015.)
⊢ (A ∈ NC → 0c ≤c A)
Theorem	ncpw1pwneg 6202	The cardinality of a unit power class is not equal to the cardinality of the power class. Theorem XI.2.4 of [Rosser] p. 372. (Contributed by SF, 10-Mar-2015.)
⊢ (A ∈ V → Nc ℘1A ≠ Nc ℘A)
Theorem	ltcpw1pwg 6203	The cardinality of a unit power class is strictly less than the cardinality of the power class. Theorem XI.2.17 of [Rosser] p. 376. (Contributed by SF, 10-Mar-2015.)
⊢ (A ∈ V → Nc ℘1A <c Nc ℘A)
Theorem	sbthlem1 6204	Lemma for sbth 6207. Set up similarity with a range. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 11-Mar-2015.)
⊢ R ∈ V    &   ⊢ X ∈ V    &   ⊢ G = Clos1 ((X ∖ ran R), R)    &   ⊢ A = (X ∩ G)    &   ⊢ B = (X ∖ G)    &   ⊢ C = (ran R ∩ G)    &   ⊢ D = (ran R ∖ G)    ⇒   ⊢ (((Fun R ∧ Fun ◡R) ∧ (X ⊆ dom R ∧ ran R ⊆ X)) → ran R ≈ X)
Theorem	sbthlem2 6205	Lemma for sbth 6207. Eliminate hypotheses from sbthlem1 6204. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 10-Mar-2015.)
⊢ R ∈ V    ⇒   ⊢ (((Fun R ∧ Fun ◡R) ∧ (B ∈ V ∧ B ⊆ dom R ∧ ran R ⊆ B)) → ran R ≈ B)
Theorem	sbthlem3 6206	Lemma for sbth 6207. If A is equinumerous with a subset of B and vice-versa, then A is equinumerous with B. Theorem XI.1.15 of [Rosser] p. 353. (Contributed by SF, 10-Mar-2015.)
⊢ (((A ≈ C ∧ C ⊆ B) ∧ (B ≈ D ∧ D ⊆ A)) → A ≈ B)
Theorem	sbth 6207	The Schroder-Bernstein Theorem. This theorem gives the antisymmetry law for cardinal less than or equal. Translated out, it means that, if A is no larger than B and B is no larger than A, then Nc A = Nc B. Theorem XI.2.20 of [Rosser] p. 376. (Contributed by SF, 11-Mar-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ) → ((A ≤c B ∧ B ≤c A) → A = B))
Theorem	ltlenlec 6208	Cardinal less than is equivalent to one-way cardinal less than or equal. Theorem XI.2.21 of [Rosser] p. 377. (Contributed by SF, 11-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → (M <c N ↔ (M ≤c N ∧ ¬ N ≤c M)))
Theorem	addlec 6209	For nonempty sets, cardinal sum always increases cardinal less than or equal. Theorem XI.2.19 of [Rosser] p. 376. (Contributed by SF, 11-Mar-2015.)
⊢ ((M ∈ V ∧ N ∈ W ∧ (M +c N) ≠ ∅) → M ≤c (M +c N))
Theorem	addlecncs 6210	For cardinals, cardinal sum always increases cardinal less than or equal. Corollary of theorem XI.2.19 of [Rosser] p. 376. (Contributed by SF, 11-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → M ≤c (M +c N))
Theorem	dflec2 6211*	Cardinal less than or equal in terms of cardinal addition. Theorem XI.2.22 of [Rosser] p. 377. (Contributed by SF, 11-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → (M ≤c N ↔ ∃p ∈ NC N = (M +c p)))
Theorem	lectr 6212	Cardinal less than or equal is transitive. (Contributed by SF, 12-Mar-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) → ((A ≤c B ∧ B ≤c C) → A ≤c C))
Theorem	leltctr 6213	Transitivity law for cardinal less than or equal and less than. (Contributed by SF, 16-Mar-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) → ((A ≤c B ∧ B <c C) → A <c C))
Theorem	lecponc 6214	Cardinal less than or equal partially orders the cardinals. (Contributed by SF, 12-Mar-2015.)
⊢ ≤c Po NC
Theorem	leaddc1 6215	Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
⊢ (((M ∈ NC ∧ N ∈ NC ∧ P ∈ NC ) ∧ M ≤c N) → (M +c P) ≤c (N +c P))
Theorem	leaddc2 6216	Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
⊢ (((M ∈ NC ∧ N ∈ NC ∧ P ∈ NC ) ∧ N ≤c P) → (M +c N) ≤c (M +c P))
Theorem	nc0le1 6217	Any cardinal is either zero or no greater than one. Theorem XI.2.24 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
⊢ (N ∈ NC → (N = 0c ∨ 1c ≤c N))
Theorem	nc0suc 6218*	Any cardinal is either zero or the successor of a cardinal. Corollary of theorem XI.2.24 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
⊢ (N ∈ NC → (N = 0c ∨ ∃m ∈ NC N = (m +c 1c)))
Theorem	leconnnc 6219	Cardinal less than or equal is total over the naturals. (Contributed by SF, 12-Mar-2015.)
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (A ≤c B ∨ B ≤c A))
Theorem	addceq0 6220	The sum of two cardinals is zero iff both addends are zero. (Contributed by SF, 12-Mar-2015.)
⊢ ((A ∈ NC ∧ B ∈ NC ) → ((A +c B) = 0c ↔ (A = 0c ∧ B = 0c)))
Theorem	ce2lt 6221	Ordering law for cardinal exponentiation to two. Theorem XI.2.71 of [Rosser] p. 390. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ (M ↑c 0c) ∈ NC ) → M <c (2c ↑c M))
Theorem	dflec3 6222*	Another potential definition of cardinal inequality. (Contributed by SF, 23-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → (M ≤c N ↔ ∃a ∈ M ∃b ∈ N ∃f f:a–1-1→b))
Theorem	nclenc 6223*	Comparison rule for cardinalities. (Contributed by SF, 24-Mar-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ( Nc A ≤c Nc B ↔ ∃f f:A–1-1→B)
Theorem	lenc 6224*	Less than or equal condition for the cardinality of a number. (Contributed by SF, 18-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ (M ∈ NC → (M ≤c Nc A ↔ ∃x ∈ M x ⊆ A))
Theorem	tcncg 6225	Compute the T-raising of a cardinality. (Contributed by SF, 23-Apr-2021.)
⊢ (A ∈ V → Tc Nc A = Nc ℘1A)
Theorem	tcnc 6226	Compute the T-raising of a cardinality. (Contributed by SF, 4-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ Tc Nc A = Nc ℘1A
Theorem	tcncv 6227	Compute the T-raising of the cardinality of the universe. Part of Theorem 5.2 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
⊢ Tc Nc V = Nc 1c
Theorem	tcnc1c 6228	Compute the T-raising of the cardinality of one. Part of Theorem 5.2 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
⊢ Tc Nc 1c = Nc ℘11c
Theorem	tc11 6229	Cardinal T is one-to-one. Based on theorem 2.4 of [Specker] p. 972. (Contributed by SF, 10-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → ( Tc M = Tc N ↔ M = N))
Theorem	taddc 6230*	T raising rule for cardinal sum. (Contributed by SF, 11-Mar-2015.)
⊢ (((A ∈ NC ∧ B ∈ NC ∧ X ∈ NC ) ∧ Tc A = ( Tc B +c X)) → ∃c ∈ NC X = Tc c)
Theorem	tlecg 6231	T-raising perserves order for cardinals. Theorem 5.5 of [Specker] p. 973. (Contributed by SF, 11-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → (M ≤c N ↔ Tc M ≤c Tc N))
Theorem	letc 6232*	If a cardinal is less than or equal to a T-raising, then it is also a T-raising. Theorem 5.6 of [Specker] p. 973. (Contributed by SF, 11-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ∧ M ≤c Tc N) → ∃p ∈ NC M = Tc p)
Theorem	ce0t 6233*	If (M ↑c 0c) is a cardinal, then M is a T-raising of some cardinal. (Contributed by SF, 17-Mar-2015.)
⊢ ((M ∈ NC ∧ (M ↑c 0c) ∈ NC ) → ∃n ∈ NC M = Tc n)
Theorem	ce2le 6234	Partial ordering law for base two cardinal exponentiation. Theorem 4.8 of [Specker] p. 973. (Contributed by SF, 16-Mar-2015.)
⊢ (((M ∈ NC ∧ N ∈ NC ∧ (N ↑c 0c) ∈ NC ) ∧ M ≤c N) → (2c ↑c M) ≤c (2c ↑c N))
Theorem	cet 6235	The exponent of a T-raising to a T-raising is always a cardinal. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → ( Tc M ↑c Tc N) ∈ NC )
Theorem	ce2t 6236	The exponent of two to a T-raising is always a cardinal. Theorem 5.8 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
⊢ (M ∈ NC → (2c ↑c Tc M) ∈ NC )
Theorem	tce2 6237	Distributive law for T-raising and cardinal exponentiation to two. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ (M ↑c 0c) ∈ NC ) → Tc (2c ↑c M) = (2c ↑c Tc M))
Theorem	te0c 6238	A T-raising raised to zero is always a cardinal. (Contributed by SF, 16-Mar-2015.)
⊢ (M ∈ NC → ( Tc M ↑c 0c) ∈ NC )
Theorem	ce0tb 6239*	(M ↑c 0c) is a cardinal iff M is a T-raising of some cardinal. (Contributed by SF, 17-Mar-2015.)
⊢ (M ∈ NC → ((M ↑c 0c) ∈ NC ↔ ∃n ∈ NC M = Tc n))
Theorem	ce0lenc1 6240	Cardinal exponentiation to zero is a cardinal iff the number is less than the size of cardinal one. (Contributed by SF, 18-Mar-2015.)
⊢ (M ∈ NC → ((M ↑c 0c) ∈ NC ↔ M ≤c Nc 1c))
Theorem	tlenc1c 6241	A T-raising is less than or equal to the cardinality of cardinal one. (Contributed by SF, 16-Mar-2015.)
⊢ (M ∈ NC → Tc M ≤c Nc 1c)
Theorem	1ne0c 6242	Cardinal one is not zero. (Contributed by SF, 4-Mar-2015.)
⊢ 1c ≠ 0c
Theorem	2ne0c 6243	Cardinal two is not zero. (Contributed by SF, 4-Mar-2015.)
⊢ 2c ≠ 0c
Theorem	finnc 6244	A set is finite iff its cardinality is a natural. (Contributed by SF, 18-Mar-2015.)
⊢ (A ∈ Fin ↔ Nc A ∈ Nn )
Theorem	tcfnex 6245	The stratified T raising function is a set. (Contributed by SF, 18-Mar-2015.)
⊢ TcFn ∈ V
Theorem	fntcfn 6246	Functionhood statement for the stratified T-raising function. (Contributed by SF, 18-Mar-2015.)
⊢ TcFn Fn 1c
Theorem	brtcfn 6247	Binary relationship form of the stratified T-raising function. (Contributed by SF, 18-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ ({A}TcFnB ↔ B = Tc A)
Theorem	ncfin 6248	The cardinality of a set is a natural iff the set is finite. (Contributed by SF, 19-Mar-2015.)
⊢ A ∈ V    ⇒   ⊢ ( Nc A ∈ Nn ↔ A ∈ Fin )
Theorem	nclennlem1 6249*	Lemma for nclenn 6250. Set up stratification for induction. (Contributed by SF, 19-Mar-2015.)
⊢ {x ∣ ∀n ∈ NC (n ≤c x → n ∈ Nn )} ∈ V
Theorem	nclenn 6250	A cardinal that is less than or equal to a natural is a natural. Theorem XI.3.3 of [Rosser] p. 391. (Contributed by SF, 19-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ Nn ∧ M ≤c N) → M ∈ Nn )
Theorem	addcdi 6251	Distributivity law for cardinal addition and multiplication. Theorem XI.2.31 of [Rosser] p. 379. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) → (A ·c (B +c C)) = ((A ·c B) +c (A ·c C)))
Theorem	addcdir 6252	Distributivity law for cardinal addition and multiplication. Theorem XI.2.30 of [Rosser] p. 379. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) → ((A +c B) ·c C) = ((A ·c C) +c (B ·c C)))
Theorem	muc0or 6253	The cardinal product of two cardinal numbers is zero iff one of the numbers is zero. Biconditional form of theorem XI.2.34 of [Rosser] p. 380. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ ((A ∈ NC ∧ B ∈ NC ) → ((A ·c B) = 0c ↔ (A = 0c ∨ B = 0c)))
Theorem	lemuc1 6254	Multiplication law for cardinal less than. Theorem XI.2.35 of [Rosser] p. 380. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) ∧ A ≤c B) → (A ·c C) ≤c (B ·c C))
Theorem	lemuc2 6255	Multiplication law for cardinal less than. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) ∧ B ≤c C) → (A ·c B) ≤c (A ·c C))
Theorem	ncslemuc 6256	A cardinal is less than or equal to its product with another. Theorem XI.2.36 of [Rosser] p. 381. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ ((M ∈ NC ∧ N ∈ NC ∧ N ≠ 0c) → M ≤c (M ·c N))
Theorem	ncvsq 6257	The product of the cardinality of V squared is just the cardinality of V. Theorem XI.2.37 of [Rosser] p. 381. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ ( Nc V ·c Nc V) = Nc V
Theorem	vvsqenvv 6258	There are exactly as many ordered pairs as there are sets. Corollary to theorem XI.2.37 of [Rosser] p. 381. (Contributed by Scott Fenton, 31-Jul-2019.)
⊢ (V × V) ≈ V
Theorem	0lt1c 6259	Cardinal one is strictly greater than cardinal zero. (Contributed by Scott Fenton, 1-Aug-2019.)
⊢ 0c <c 1c
Theorem	csucex 6260	The function mapping x to its cardinal successor exists. (Contributed by Scott Fenton, 30-Jul-2019.)
⊢ (x ∈ V ↦ (x +c 1c)) ∈ V
Theorem	brcsuc 6261*	Binary relationship form of the successor mapping function. (Contributed by Scott Fenton, 2-Aug-2019.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (A(x ∈ V ↦ (x +c 1c))B ↔ B = (A +c 1c))
Theorem	nnltp1clem1 6262	Lemma for nnltp1c 6263. Set up stratification. (Contributed by SF, 25-Mar-2015.)
⊢ {x ∣ x <c (x +c 1c)} ∈ V
Theorem	nnltp1c 6263	Any natural is less than one plus itself. (Contributed by SF, 25-Mar-2015.)
⊢ (N ∈ Nn → N <c (N +c 1c))
Theorem	addccan2nclem1 6264*	Lemma for addccan2nc 6266. Stratification helper theorem. (Contributed by Scott Fenton, 2-Aug-2019.)
⊢ (x( AddC ∘ ◡(1st ↾ (V × {n})))y ↔ y = (x +c n))
Theorem	addccan2nclem2 6265*	Lemma for addccan2nc 6266. Establish stratification for induction. (Contributed by Scott Fenton, 2-Aug-2019.)
⊢ ((N ∈ V ∧ P ∈ W) → {x ∣ ((x +c N) = (x +c P) → N = P)} ∈ V)
Theorem	addccan2nc 6266	Cancellation law for addition over the cardinal numbers. Biconditional form of theorem XI.3.2 of [Rosser] p. 391. (Contributed by Scott Fenton, 2-Aug-2019.)
⊢ ((M ∈ Nn ∧ N ∈ NC ∧ P ∈ NC ) → ((M +c N) = (M +c P) ↔ N = P))
Theorem	lecadd2 6267	Cardinal addition preserves cardinal less than. Biconditional form of corollary 4 of theorem XI.3.2 of [Rosser] p. 391. (Contributed by Scott Fenton, 2-Aug-2019.)
⊢ ((M ∈ Nn ∧ N ∈ NC ∧ P ∈ NC ) → ((M +c N) ≤c (M +c P) ↔ N ≤c P))
Theorem	ncslesuc 6268	Relationship between successor and cardinal less than or equal. (Contributed by Scott Fenton, 3-Aug-2019.)
⊢ ((M ∈ NC ∧ N ∈ NC ) → (M ≤c (N +c 1c) ↔ (M ≤c N ∨ M = (N +c 1c))))
Theorem	nmembers1lem1 6269*	Lemma for nmembers1 6272. Set up stratification. (Contributed by SF, 25-Mar-2015.)
⊢ {x ∣ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ Tc Tc x} ∈ V
Theorem	nmembers1lem2 6270	Lemma for nmembers1 6272. The set of all elements between one and zero is empty. (Contributed by Scott Fenton, 1-Aug-2019.)
⊢ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c 0c)} ∈ 0c
Theorem	nmembers1lem3 6271*	Lemma for nmembers1 6272. If the interval from one to a natural is in a given natural, extending it by one puts it in the next natural. (Contributed by Scott Fenton, 3-Aug-2019.)
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ({m ∈ Nn ∣ (1c ≤c m ∧ m ≤c A)} ∈ B → {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c (A +c 1c))} ∈ (B +c 1c)))
Theorem	nmembers1 6272*	Count the number of elements in a natural interval. From nmembers1lem2 6270 and nmembers1lem3 6271, we would expect to arrive at {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c N)} ∈ N, but this proposition is not stratifiable. Instead, we arrive at the weaker conclusion below. We can arrive at the earlier proposition once we add the Axiom of Counting, which we will do later. (Contributed by Scott Fenton, 3-Aug-2019.)
⊢ (N ∈ Nn → {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c N)} ∈ Tc Tc N)
Theorem	ltcirr 6273	Cardinal less than is irreflexive. (Contributed by Scott Fenton, 12-Dec-2021.)
⊢ ¬ A <c A
2.4.6  Specker's disproof of the axiom of choice
Syntax	cspac 6274	Extend the definition of a class to include the special set generator for the axiom of choice.
class Spac
Definition	df-spac 6275*	Define the special class generator for the disproof of the axiom of choice. Definition 6.1 of [Specker] p. 973. (Contributed by SF, 3-Mar-2015.)
⊢ Spac = (m ∈ NC ↦ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
Theorem	nncdiv3lem1 6276	Lemma for nncdiv3 6278. Set up a helper for stratification. (Contributed by SF, 3-Mar-2015.)
⊢ (⟨n, b⟩ ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd )) “ AddC )) ↔ b = ((n +c n) +c n))
Theorem	nncdiv3lem2 6277*	Lemma for nncdiv3 6278. Set up stratification for induction. (Contributed by SF, 2-Mar-2015.)
⊢ {a ∣ ∃n ∈ Nn (a = ((n +c n) +c n) ∨ a = (((n +c n) +c n) +c 1c) ∨ a = (((n +c n) +c n) +c 2c))} ∈ V
Theorem	nncdiv3 6278*	Divisibility by three rule for finite cardinals. Part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 2-Mar-2015.)
⊢ (A ∈ Nn → ∃n ∈ Nn (A = ((n +c n) +c n) ∨ A = (((n +c n) +c n) +c 1c) ∨ A = (((n +c n) +c n) +c 2c)))
Theorem	nnc3n3p1 6279	Three times a natural is not one more than three times a natural. Another part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬ ((A +c A) +c A) = (((B +c B) +c B) +c 1c))
Theorem	nnc3n3p2 6280	Three times a natural is not two more than three times a natural. Another part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 12-Mar-2015.)
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬ ((A +c A) +c A) = (((B +c B) +c B) +c 2c))
Theorem	nnc3p1n3p2 6281	One more than three times a natural is not two more than three times a natural. Final part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 12-Mar-2015.)
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬ (((A +c A) +c A) +c 1c) = (((B +c B) +c B) +c 2c))
Theorem	spacvallem1 6282*	Lemma for spacval 6283. Set up stratification for the recursive relationship. (Contributed by SF, 6-Mar-2015.)
⊢ {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))} ∈ V
Theorem	spacval 6283*	The value of the special set generator. (Contributed by SF, 4-Mar-2015.)
⊢ (N ∈ NC → ( Spac ‘N) = Clos1 ({N}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c x))}))
Theorem	fnspac 6284	The special set generator is a function over the cardinals. (Contributed by SF, 18-Mar-2015.)
⊢ Spac Fn NC
Theorem	spacssnc 6285	The special set generator generates a set of cardinals. (Contributed by SF, 13-Mar-2015.)
⊢ (N ∈ NC → ( Spac ‘N) ⊆ NC )
Theorem	spacid 6286	The initial value of the special set generator is an element. (Contributed by SF, 13-Mar-2015.)
⊢ (M ∈ NC → M ∈ ( Spac ‘M))
Theorem	spaccl 6287	Closure law for the special set generator. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M) ∧ (N ↑c 0c) ∈ NC ) → (2c ↑c N) ∈ ( Spac ‘M))
Theorem	spacind 6288*	Inductive law for the special set generator. (Contributed by SF, 13-Mar-2015.)
⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x ↑c 0c) ∈ NC ) → (2c ↑c x) ∈ S))) → ( Spac ‘M) ⊆ S)
Theorem	spacis 6289*	Induction scheme for the special set generator. (Contributed by SF, 13-Mar-2015.)
⊢ {x ∣ φ} ∈ V    &   ⊢ (x = M → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (2c ↑c y) → (φ ↔ θ))    &   ⊢ (x = N → (φ ↔ τ))    &   ⊢ (M ∈ NC → ψ)    &   ⊢ (((M ∈ NC ∧ y ∈ ( Spac ‘M)) ∧ ((y ↑c 0c) ∈ NC ∧ χ)) → θ)    ⇒   ⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M)) → τ)
Theorem	nchoicelem1 6290	Lemma for nchoice 6309. A finite cardinal is not one more than its T-raising. (Contributed by SF, 3-Mar-2015.)
⊢ (A ∈ Nn → ¬ A = ( Tc A +c 1c))
Theorem	nchoicelem2 6291	Lemma for nchoice 6309. A finite cardinal is not two more than its T-raising. (Contributed by SF, 12-Mar-2015.)
⊢ (A ∈ Nn → ¬ A = ( Tc A +c 2c))
Theorem	nchoicelem3 6292	Lemma for nchoice 6309. Compute the value of Spac when the argument is not exponentiable. Theorem 6.2 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ ¬ (M ↑c 0c) ∈ NC ) → ( Spac ‘M) = {M})
Theorem	nchoicelem4 6293	Lemma for nchoice 6309. The initial value of Spac is a minimum value. Theorem 6.4 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M)) → M ≤c N)
Theorem	nchoicelem5 6294	Lemma for nchoice 6309. A cardinal is not a member of the special set of itself raised to two. Theorem 6.5 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ (M ↑c 0c) ∈ NC ) → ¬ M ∈ ( Spac ‘(2c ↑c M)))
Theorem	nchoicelem6 6295	Lemma for nchoice 6309. Split the special set generator into base and inductive values. Theorem 6.6 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ (M ↑c 0c) ∈ NC ) → ( Spac ‘M) = ({M} ∪ ( Spac ‘(2c ↑c M))))
Theorem	nchoicelem7 6296	Lemma for nchoice 6309. Calculate the cardinality of a special set generator. Theorem 6.7 of [Specker] p. 974. (Contributed by SF, 13-Mar-2015.)
⊢ ((M ∈ NC ∧ (M ↑c 0c) ∈ NC ) → Nc ( Spac ‘M) = ( Nc ( Spac ‘(2c ↑c M)) +c 1c))
Theorem	nchoicelem8 6297	Lemma for nchoice 6309. An anti-closure condition for cardinal exponentiation to zero. Theorem 4.5 of [Specker] p. 973. (Contributed by SF, 18-Mar-2015.)
⊢ (( ≤c We NC ∧ M ∈ NC ) → (¬ (M ↑c 0c) ∈ NC ↔ Nc 1c <c M))
Theorem	nchoicelem9 6298	Lemma for nchoice 6309. Calculate the cardinality of the special set generator when near the end of raisability. Theorem 6.8 of [Specker] p. 974. (Contributed by SF, 18-Mar-2015.)
⊢ (( ≤c We NC ∧ M ∈ NC ∧ ¬ (M ↑c 0c) ∈ NC ) → ( Nc ( Spac ‘ Tc M) = 2c ∨ Nc ( Spac ‘ Tc M) = 3c))
Theorem	nchoicelem10 6299	Lemma for nchoice 6309. Stratification helper lemma. (Contributed by SF, 18-Mar-2015.)
⊢ S ∈ V    &   ⊢ X ∈ V    ⇒   ⊢ (⟨c, X⟩ ∈ ∼ (( Ins3 S ⊕ Ins2 ∼ ran (◡ ∼ S ⊗ (◡ S ↾ Fix ( S ∘ ImageS)))) “ 1c) ↔ c = Clos1 (X, S))
Theorem	nchoicelem11 6300*	Lemma for nchoice 6309. Set up stratification for nchoicelem12 6301. (Contributed by SF, 18-Mar-2015.)
⊢ {t ∣ ∀m ∈ NC (t = Nc ( Spac ‘ Tc m) → Nc ( Spac ‘m) ∈ Nn )} ∈ V