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	ncpw1pwneg 6201	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 e. V -> Nc ~P1 A =/= Nc ~PA)
Theorem	ltcpw1pwg 6202	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 e. V -> Nc ~P1 A <c Nc ~PA)
Theorem	sbthlem1 6203	Lemma for sbth 6206. Set up similarity with a range. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 11-Mar-2015.)
|- R e. _V   &   |- X e. _V   &   |- G = Clos1 ((X \ ran R), R)   &   |- A = (X i^i G)   &   |- B = (X \ G)   &   |- C = (ran R i^i G)   &   |- D = (ran R \ G)   =>   |- (((Fun R /\ Fun `'R) /\ (X C_ dom R /\ ran R C_ X)) -> ran R ~~ X)
Theorem	sbthlem2 6204	Lemma for sbth 6206. Eliminate hypotheses from sbthlem1 6203. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 10-Mar-2015.)
|- R e. _V   =>   |- (((Fun R /\ Fun `'R) /\ (B e. V /\ B C_ dom R /\ ran R C_ B)) -> ran R ~~ B)
Theorem	sbthlem3 6205	Lemma for sbth 6206. 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 C_ B) /\ (B ~~ D /\ D C_ A)) -> A ~~ B)
Theorem	sbth 6206	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 e. NC /\ B e. NC ) -> ((A <_c B /\ B <_c A) -> A = B))
Theorem	ltlenlec 6207	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 e. NC /\ N e. NC ) -> (M <c N <-> (M <_c N /\ -. N <_c M)))
Theorem	addlec 6208	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 e. V /\ N e. W /\ (M +o N) =/= (/)) -> M <_c (M +o N))
Theorem	addlecncs 6209	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 e. NC /\ N e. NC ) -> M <_c (M +o N))
Theorem	dflec2 6210*	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 e. NC /\ N e. NC ) -> (M <_c N <-> E.p e. NC N = (M +o p)))
Theorem	lectr 6211	Cardinal less than or equal is transitive. (Contributed by SF, 12-Mar-2015.)
|- ((A e. NC /\ B e. NC /\ C e. NC ) -> ((A <_c B /\ B <_c C) -> A <_c C))
Theorem	leltctr 6212	Transitivity law for cardinal less than or equal and less than. (Contributed by SF, 16-Mar-2015.)
|- ((A e. NC /\ B e. NC /\ C e. NC ) -> ((A <_c B /\ B <c C) -> A <c C))
Theorem	lecponc 6213	Cardinal less than or equal partially orders the cardinals. (Contributed by SF, 12-Mar-2015.)
|- <_c Po NC
Theorem	leaddc1 6214	Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
|- (((M e. NC /\ N e. NC /\ P e. NC ) /\ M <_c N) -> (M +o P) <_c (N +o P))
Theorem	leaddc2 6215	Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
|- (((M e. NC /\ N e. NC /\ P e. NC ) /\ N <_c P) -> (M +o N) <_c (M +o P))
Theorem	nc0le1 6216	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 e. NC -> (N = 0c \/ 1c <_c N))
Theorem	nc0suc 6217*	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 e. NC -> (N = 0c \/ E.m e. NC N = (m +o 1c)))
Theorem	leconnnc 6218	Cardinal less than or equal is total over the naturals. (Contributed by SF, 12-Mar-2015.)
|- ((A e. Nn /\ B e. Nn ) -> (A <_c B \/ B <_c A))
Theorem	addceq0 6219	The sum of two cardinals is zero iff both addends are zero. (Contributed by SF, 12-Mar-2015.)
|- ((A e. NC /\ B e. NC ) -> ((A +o B) = 0c <-> (A = 0c /\ B = 0c)))
Theorem	ce2lt 6220	Ordering law for cardinal exponentiation to two. Theorem XI.2.71 of [Rosser] p. 390. (Contributed by SF, 13-Mar-2015.)
|- ((M e. NC /\ (M ↑c 0c) e. NC ) -> M <c (2c ↑c M))
Theorem	dflec3 6221*	Another potential definition of cardinal inequality. (Contributed by SF, 23-Mar-2015.)
|- ((M e. NC /\ N e. NC ) -> (M <_c N <-> E.a e. M E.b e. N E.f f:a-1-1->b))
Theorem	nclenc 6222*	Comparison rule for cardinalities. (Contributed by SF, 24-Mar-2015.)
|- A e. _V   &   |- B e. _V   =>   |- ( Nc A <_c Nc B <-> E.f f:A-1-1->B)
Theorem	lenc 6223*	Less than or equal condition for the cardinality of a number. (Contributed by SF, 18-Mar-2015.)
|- A e. _V   =>   |- (M e. NC -> (M <_c Nc A <-> E.x e. M x C_ A))
Theorem	tcncg 6224	Compute the T-raising of a cardinality. (Contributed by SF, 23-Apr-2021.)
|- (A e. V -> Tc Nc A = Nc ~P1 A)
Theorem	tcnc 6225	Compute the T-raising of a cardinality. (Contributed by SF, 4-Mar-2015.)
|- A e. _V   =>   |- Tc Nc A = Nc ~P1 A
Theorem	tcncv 6226	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 6227	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 ~P1 1c
Theorem	tc11 6228	Cardinal T is one-to-one. Based on theorem 2.4 of [Specker] p. 972. (Contributed by SF, 10-Mar-2015.)
|- ((M e. NC /\ N e. NC ) -> ( Tc M = Tc N <-> M = N))
Theorem	taddc 6229*	T raising rule for cardinal sum. (Contributed by SF, 11-Mar-2015.)
|- (((A e. NC /\ B e. NC /\ X e. NC ) /\ Tc A = ( Tc B +o X)) -> E.c e. NC X = Tc c)
Theorem	tlecg 6230	T-raising perserves order for cardinals. Theorem 5.5 of [Specker] p. 973. (Contributed by SF, 11-Mar-2015.)
|- ((M e. NC /\ N e. NC ) -> (M <_c N <-> Tc M <_c Tc N))
Theorem	letc 6231*	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 e. NC /\ N e. NC /\ M <_c Tc N) -> E.p e. NC M = Tc p)
Theorem	ce0t 6232*	If (M ↑c 0c) is a cardinal, then M is a T-raising of some cardinal. (Contributed by SF, 17-Mar-2015.)
|- ((M e. NC /\ (M ↑c 0c) e. NC ) -> E.n e. NC M = Tc n)
Theorem	ce2le 6233	Partial ordering law for base two cardinal exponentiation. Theorem 4.8 of [Specker] p. 973. (Contributed by SF, 16-Mar-2015.)
|- (((M e. NC /\ N e. NC /\ (N ↑c 0c) e. NC ) /\ M <_c N) -> (2c ↑c M) <_c (2c ↑c N))
Theorem	cet 6234	The exponent of a T-raising to a T-raising is always a cardinal. (Contributed by SF, 13-Mar-2015.)
|- ((M e. NC /\ N e. NC ) -> ( Tc M ↑c Tc N) e. NC )
Theorem	ce2t 6235	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 e. NC -> (2c ↑c Tc M) e. NC )
Theorem	tce2 6236	Distributive law for T-raising and cardinal exponentiation to two. (Contributed by SF, 13-Mar-2015.)
|- ((M e. NC /\ (M ↑c 0c) e. NC ) -> Tc (2c ↑c M) = (2c ↑c Tc M))
Theorem	te0c 6237	A T-raising raised to zero is always a cardinal. (Contributed by SF, 16-Mar-2015.)
|- (M e. NC -> ( Tc M ↑c 0c) e. NC )
Theorem	ce0tb 6238*	(M ↑c 0c) is a cardinal iff M is a T-raising of some cardinal. (Contributed by SF, 17-Mar-2015.)
|- (M e. NC -> ((M ↑c 0c) e. NC <-> E.n e. NC M = Tc n))
Theorem	ce0lenc1 6239	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 e. NC -> ((M ↑c 0c) e. NC <-> M <_c Nc 1c))
Theorem	tlenc1c 6240	A T-raising is less than or equal to the cardinality of cardinal one. (Contributed by SF, 16-Mar-2015.)
|- (M e. NC -> Tc M <_c Nc 1c)
Theorem	1ne0c 6241	Cardinal one is not zero. (Contributed by SF, 4-Mar-2015.)
|- 1c =/= 0c
Theorem	2ne0c 6242	Cardinal two is not zero. (Contributed by SF, 4-Mar-2015.)
|- 2c =/= 0c
Theorem	finnc 6243	A set is finite iff its cardinality is a natural. (Contributed by SF, 18-Mar-2015.)
|- (A e. Fin <-> Nc A e. Nn )
Theorem	tcfnex 6244	The stratified T raising function is a set. (Contributed by SF, 18-Mar-2015.)
|- TcFn e. _V
Theorem	fntcfn 6245	Functionhood statement for the stratified T-raising function. (Contributed by SF, 18-Mar-2015.)
|- TcFn Fn 1c
Theorem	brtcfn 6246	Binary relationship form of the stratified T-raising function. (Contributed by SF, 18-Mar-2015.)
|- A e. _V   =>   |- ({A}TcFnB <-> B = Tc A)
Theorem	ncfin 6247	The cardinality of a set is a natural iff the set is finite. (Contributed by SF, 19-Mar-2015.)
|- A e. _V   =>   |- ( Nc A e. Nn <-> A e. Fin )
Theorem	nclennlem1 6248*	Lemma for nclenn 6249. Set up stratification for induction. (Contributed by SF, 19-Mar-2015.)
|- {x | A.n e. NC (n <_c x -> n e. Nn )} e. _V
Theorem	nclenn 6249	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 e. NC /\ N e. Nn /\ M <_c N) -> M e. Nn )
Theorem	addcdi 6250	Distributivity law for cardinal addition and multiplication. Theorem XI.2.31 of [Rosser] p. 379. (Contributed by Scott Fenton, 31-Jul-2019.)
|- ((A e. NC /\ B e. NC /\ C e. NC ) -> (A ·c (B +o C)) = ((A ·c B) +o (A ·c C)))
Theorem	addcdir 6251	Distributivity law for cardinal addition and multiplication. Theorem XI.2.30 of [Rosser] p. 379. (Contributed by Scott Fenton, 31-Jul-2019.)
|- ((A e. NC /\ B e. NC /\ C e. NC ) -> ((A +o B) ·c C) = ((A ·c C) +o (B ·c C)))
Theorem	muc0or 6252	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 e. NC /\ B e. NC ) -> ((A ·c B) = 0c <-> (A = 0c \/ B = 0c)))
Theorem	lemuc1 6253	Multiplication law for cardinal less than. Theorem XI.2.35 of [Rosser] p. 380. (Contributed by Scott Fenton, 31-Jul-2019.)
|- (((A e. NC /\ B e. NC /\ C e. NC ) /\ A <_c B) -> (A ·c C) <_c (B ·c C))
Theorem	lemuc2 6254	Multiplication law for cardinal less than. (Contributed by Scott Fenton, 31-Jul-2019.)
|- (((A e. NC /\ B e. NC /\ C e. NC ) /\ B <_c C) -> (A ·c B) <_c (A ·c C))
Theorem	ncslemuc 6255	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 e. NC /\ N e. NC /\ N =/= 0c) -> M <_c (M ·c N))
Theorem	ncvsq 6256	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 6257	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 X. _V) ~~ _V
Theorem	0lt1c 6258	Cardinal one is strictly greater than cardinal zero. (Contributed by Scott Fenton, 1-Aug-2019.)
|- 0c <c 1c
Theorem	csucex 6259	The function mapping x to its cardinal successor exists. (Contributed by Scott Fenton, 30-Jul-2019.)
|- (x e. _V |-> (x +o 1c)) e. _V
Theorem	brcsuc 6260*	Binary relationship form of the successor mapping function. (Contributed by Scott Fenton, 2-Aug-2019.)
|- A e. _V   &   |- B e. _V   =>   |- (A(x e. _V |-> (x +o 1c))B <-> B = (A +o 1c))
Theorem	nnltp1clem1 6261	Lemma for nnltp1c 6262. Set up stratification. (Contributed by SF, 25-Mar-2015.)
|- {x | x <c (x +o 1c)} e. _V
Theorem	nnltp1c 6262	Any natural is less than one plus itself. (Contributed by SF, 25-Mar-2015.)
|- (N e. Nn -> N <c (N +o 1c))
Theorem	addccan2nclem1 6263*	Lemma for addccan2nc 6265. Stratification helper theorem. (Contributed by Scott Fenton, 2-Aug-2019.)
|- (x( AddC o. `'(1st |` (_V X. {n})))y <-> y = (x +o n))
Theorem	addccan2nclem2 6264*	Lemma for addccan2nc 6265. Establish stratification for induction. (Contributed by Scott Fenton, 2-Aug-2019.)
|- ((N e. V /\ P e. W) -> {x | ((x +o N) = (x +o P) -> N = P)} e. _V)
Theorem	addccan2nc 6265	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 e. Nn /\ N e. NC /\ P e. NC ) -> ((M +o N) = (M +o P) <-> N = P))
Theorem	lecadd2 6266	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 e. Nn /\ N e. NC /\ P e. NC ) -> ((M +o N) <_c (M +o P) <-> N <_c P))
Theorem	ncslesuc 6267	Relationship between successor and cardinal less than or equal. (Contributed by Scott Fenton, 3-Aug-2019.)
|- ((M e. NC /\ N e. NC ) -> (M <_c (N +o 1c) <-> (M <_c N \/ M = (N +o 1c))))
Theorem	nmembers1lem1 6268*	Lemma for nmembers1 6271. Set up stratification. (Contributed by SF, 25-Mar-2015.)
|- {x | {m e. Nn | (1c <_c m /\ m <_c x)} e. Tc Tc x} e. _V
Theorem	nmembers1lem2 6269	Lemma for nmembers1 6271. The set of all elements between one and zero is empty. (Contributed by Scott Fenton, 1-Aug-2019.)
|- {m e. Nn | (1c <_c m /\ m <_c 0c)} e. 0c
Theorem	nmembers1lem3 6270*	Lemma for nmembers1 6271. 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 e. Nn /\ B e. Nn ) -> ({m e. Nn | (1c <_c m /\ m <_c A)} e. B -> {m e. Nn | (1c <_c m /\ m <_c (A +o 1c))} e. (B +o 1c)))
Theorem	nmembers1 6271*	Count the number of elements in a natural interval. From nmembers1lem2 6269 and nmembers1lem3 6270, we would expect to arrive at {m e. Nn | (1c <_c m /\ m <_c N)} e. 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 e. Nn -> {m e. Nn | (1c <_c m /\ m <_c N)} e. Tc Tc N)
Theorem	ltcirr 6272	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 6273	Extend the definition of a class to include the special set generator for the axiom of choice.
class Spac
Definition	df-spac 6274*	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 e. NC |-> Clos1 ({m}, {<.x, y>. | (x e. NC /\ y e. NC /\ y = (2c ↑c x))}))
Theorem	nncdiv3lem1 6275	Lemma for nncdiv3 6277. Set up a helper for stratification. (Contributed by SF, 3-Mar-2015.)
|- (<.n, b>. e. ran ( Ins3 `'((ran (`'1st (x) (1st i^i 2nd)) (x) 2nd)" AddC ) i^i (((1st o. 1st) (x) ((2nd o. 1st) (x) 2nd))" AddC )) <-> b = ((n +o n) +o n))
Theorem	nncdiv3lem2 6276*	Lemma for nncdiv3 6277. Set up stratification for induction. (Contributed by SF, 2-Mar-2015.)
|- {a | E.n e. Nn (a = ((n +o n) +o n) \/ a = (((n +o n) +o n) +o 1c) \/ a = (((n +o n) +o n) +o 2c))} e. _V
Theorem	nncdiv3 6277*	Divisibility by three rule for finite cardinals. Part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 2-Mar-2015.)
|- (A e. Nn -> E.n e. Nn (A = ((n +o n) +o n) \/ A = (((n +o n) +o n) +o 1c) \/ A = (((n +o n) +o n) +o 2c)))
Theorem	nnc3n3p1 6278	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 e. Nn /\ B e. Nn ) -> -. ((A +o A) +o A) = (((B +o B) +o B) +o 1c))
Theorem	nnc3n3p2 6279	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 e. Nn /\ B e. Nn ) -> -. ((A +o A) +o A) = (((B +o B) +o B) +o 2c))
Theorem	nnc3p1n3p2 6280	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 e. Nn /\ B e. Nn ) -> -. (((A +o A) +o A) +o 1c) = (((B +o B) +o B) +o 2c))
Theorem	spacvallem1 6281*	Lemma for spacval 6282. Set up stratification for the recursive relationship. (Contributed by SF, 6-Mar-2015.)
|- {<.x, y>. | (x e. NC /\ y e. NC /\ y = (2c ↑c x))} e. _V
Theorem	spacval 6282*	The value of the special set generator. (Contributed by SF, 4-Mar-2015.)
|- (N e. NC -> ( Spac ` N) = Clos1 ({N}, {<.x, y>. | (x e. NC /\ y e. NC /\ y = (2c ↑c x))}))
Theorem	fnspac 6283	The special set generator is a function over the cardinals. (Contributed by SF, 18-Mar-2015.)
|- Spac Fn NC
Theorem	spacssnc 6284	The special set generator generates a set of cardinals. (Contributed by SF, 13-Mar-2015.)
|- (N e. NC -> ( Spac ` N) C_ NC )
Theorem	spacid 6285	The initial value of the special set generator is an element. (Contributed by SF, 13-Mar-2015.)
|- (M e. NC -> M e. ( Spac ` M))
Theorem	spaccl 6286	Closure law for the special set generator. (Contributed by SF, 13-Mar-2015.)
|- ((M e. NC /\ N e. ( Spac ` M) /\ (N ↑c 0c) e. NC ) -> (2c ↑c N) e. ( Spac ` M))
Theorem	spacind 6287*	Inductive law for the special set generator. (Contributed by SF, 13-Mar-2015.)
|- (((M e. NC /\ S e. V) /\ (M e. S /\ A.x e. ( Spac ` M)((x e. S /\ (x ↑c 0c) e. NC ) -> (2c ↑c x) e. S))) -> ( Spac ` M) C_ S)
Theorem	spacis 6288*	Induction scheme for the special set generator. (Contributed by SF, 13-Mar-2015.)
|- {x | ph} e. _V   &   |- (x = M -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = (2c ↑c y) -> (ph <-> th))   &   |- (x = N -> (ph <-> ta))   &   |- (M e. NC -> ps)   &   |- (((M e. NC /\ y e. ( Spac ` M)) /\ ((y ↑c 0c) e. NC /\ ch)) -> th)   =>   |- ((M e. NC /\ N e. ( Spac ` M)) -> ta)
Theorem	nchoicelem1 6289	Lemma for nchoice 6308. A finite cardinal is not one more than its T-raising. (Contributed by SF, 3-Mar-2015.)
|- (A e. Nn -> -. A = ( Tc A +o 1c))
Theorem	nchoicelem2 6290	Lemma for nchoice 6308. A finite cardinal is not two more than its T-raising. (Contributed by SF, 12-Mar-2015.)
|- (A e. Nn -> -. A = ( Tc A +o 2c))
Theorem	nchoicelem3 6291	Lemma for nchoice 6308. 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 e. NC /\ -. (M ↑c 0c) e. NC ) -> ( Spac ` M) = {M})
Theorem	nchoicelem4 6292	Lemma for nchoice 6308. The initial value of Spac is a minimum value. Theorem 6.4 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
|- ((M e. NC /\ N e. ( Spac ` M)) -> M <_c N)
Theorem	nchoicelem5 6293	Lemma for nchoice 6308. 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 e. NC /\ (M ↑c 0c) e. NC ) -> -. M e. ( Spac ` (2c ↑c M)))
Theorem	nchoicelem6 6294	Lemma for nchoice 6308. Split the special set generator into base and inductive values. Theorem 6.6 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
|- ((M e. NC /\ (M ↑c 0c) e. NC ) -> ( Spac ` M) = ({M} u. ( Spac ` (2c ↑c M))))
Theorem	nchoicelem7 6295	Lemma for nchoice 6308. Calculate the cardinality of a special set generator. Theorem 6.7 of [Specker] p. 974. (Contributed by SF, 13-Mar-2015.)
|- ((M e. NC /\ (M ↑c 0c) e. NC ) -> Nc ( Spac ` M) = ( Nc ( Spac ` (2c ↑c M)) +o 1c))
Theorem	nchoicelem8 6296	Lemma for nchoice 6308. 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 e. NC ) -> (-. (M ↑c 0c) e. NC <-> Nc 1c <c M))
Theorem	nchoicelem9 6297	Lemma for nchoice 6308. 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 e. NC /\ -. (M ↑c 0c) e. NC ) -> ( Nc ( Spac ` Tc M) = 2c \/ Nc ( Spac ` Tc M) = 3c))
Theorem	nchoicelem10 6298	Lemma for nchoice 6308. Stratification helper lemma. (Contributed by SF, 18-Mar-2015.)
|- S e. _V   &   |- X e. _V   =>   |- (<.c, X>. e. ∼ (( Ins3 S (+) Ins2 ∼ ran (`' ∼ S (x) (`' S |` Fix( S o. ImageS))))"1c) <-> c = Clos1 (X, S))
Theorem	nchoicelem11 6299*	Lemma for nchoice 6308. Set up stratification for nchoicelem12 6300. (Contributed by SF, 18-Mar-2015.)
|- {t | A.m e. NC (t = Nc ( Spac ` Tc m) -> Nc ( Spac ` m) e. Nn )} e. _V
Theorem	nchoicelem12 6300	Lemma for nchoice 6308. 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 e. NC /\ ( Spac ` Tc M) e. Fin ) -> ( Spac ` M) e. Fin )