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,
10Mar2015.)

⊢ (A ∈ V →
Nc ℘_{1}A ≠ Nc ℘A) 

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, 10Mar2015.)

⊢ (A ∈ V →
Nc ℘_{1}A <_{c} Nc
℘A) 

Theorem  sbthlem1 6203 
Lemma for sbth 6206. Set up similarity with a range. Theorem
XI.1.14 of
[Rosser] p. 350. (Contributed by SF,
11Mar2015.)

⊢ 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 6204 
Lemma for sbth 6206. Eliminate hypotheses from sbthlem1 6203. Theorem
XI.1.14 of [Rosser] p. 350. (Contributed
by SF, 10Mar2015.)

⊢ R ∈ V ⇒ ⊢ (((Fun R
∧ Fun ^{◡}R)
∧ (B
∈ V
∧ B ⊆ dom R ∧ ran R ⊆ B)) →
ran R ≈ B) 

Theorem  sbthlem3 6205 
Lemma for sbth 6206. If A is equinumerous with a subset of B and
viceversa, then A is
equinumerous with B. Theorem
XI.1.15 of
[Rosser] p. 353. (Contributed by SF,
10Mar2015.)

⊢ (((A
≈ C ∧ C ⊆ B) ∧ (B ≈
D ∧
D ⊆
A)) → A ≈ B) 

Theorem  sbth 6206 
The SchroderBernstein 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, 11Mar2015.)

⊢ ((A ∈ NC ∧ B ∈ NC ) →
((A ≤_{c} B ∧ B ≤_{c} A) → A =
B)) 

Theorem  ltlenlec 6207 
Cardinal less than is equivalent to oneway cardinal less than or equal.
Theorem XI.2.21 of [Rosser] p. 377.
(Contributed by SF, 11Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ 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,
11Mar2015.)

⊢ ((M ∈ V ∧ N ∈ W ∧ (M
+_{c} N) ≠ ∅) → M
≤_{c} (M +_{c}
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,
11Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ NC ) →
M ≤_{c} (M +_{c} 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, 11Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M ≤_{c} N ↔ ∃p ∈ NC N = (M
+_{c} p))) 

Theorem  lectr 6211 
Cardinal less than or equal is transitive. (Contributed by SF,
12Mar2015.)

⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ 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, 16Mar2015.)

⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ 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, 12Mar2015.)

⊢ ≤_{c} Po NC 

Theorem  leaddc1 6214 
Addition law for cardinal less than. Theorem XI.2.23 of [Rosser]
p. 377. (Contributed by SF, 12Mar2015.)

⊢ (((M ∈ NC ∧ N ∈ NC ∧ P ∈ NC ) ∧ M
≤_{c} N) → (M +_{c} P) ≤_{c} (N +_{c} P)) 

Theorem  leaddc2 6215 
Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377.
(Contributed by SF, 12Mar2015.)

⊢ (((M ∈ NC ∧ N ∈ NC ∧ P ∈ NC ) ∧ N
≤_{c} P) → (M +_{c} N) ≤_{c} (M +_{c} 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,
12Mar2015.)

⊢ (N ∈ NC → (N = 0_{c}
∨ 1_{c} ≤_{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,
12Mar2015.)

⊢ (N ∈ NC → (N = 0_{c}
∨ ∃m ∈ NC N = (m +_{c}
1_{c}))) 

Theorem  leconnnc 6218 
Cardinal less than or equal is total over the naturals. (Contributed by
SF, 12Mar2015.)

⊢ ((A ∈ Nn ∧ B ∈ 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, 12Mar2015.)

⊢ ((A ∈ NC ∧ B ∈ NC ) →
((A +_{c} B) = 0_{c} ↔ (A = 0_{c} ∧ B =
0_{c}))) 

Theorem  ce2lt 6220 
Ordering law for cardinal exponentiation to two. Theorem XI.2.71 of
[Rosser] p. 390. (Contributed by SF,
13Mar2015.)

⊢ ((M ∈ NC ∧ (M
↑_{c} 0_{c}) ∈ NC ) →
M <_{c} (2_{c}
↑_{c} M)) 

Theorem  dflec3 6221* 
Another potential definition of cardinal inequality. (Contributed by
SF, 23Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M ≤_{c} N ↔ ∃a ∈ M ∃b ∈ N ∃f f:a–11→b)) 

Theorem  nclenc 6222* 
Comparison rule for cardinalities. (Contributed by SF, 24Mar2015.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ( Nc A ≤_{c} Nc
B ↔ ∃f f:A–11→B) 

Theorem  lenc 6223* 
Less than or equal condition for the cardinality of a number.
(Contributed by SF, 18Mar2015.)

⊢ A ∈ V ⇒ ⊢ (M ∈ NC → (M ≤_{c} Nc
A ↔ ∃x ∈ M x ⊆ A)) 

Theorem  tcncg 6224 
Compute the Traising of a cardinality. (Contributed by SF,
23Apr2021.)

⊢ (A ∈ V →
T_{c} Nc
A = Nc ℘_{1}A) 

Theorem  tcnc 6225 
Compute the Traising of a cardinality. (Contributed by SF,
4Mar2015.)

⊢ A ∈ V ⇒ ⊢ T_{c}
Nc A = Nc ℘_{1}A 

Theorem  tcncv 6226 
Compute the Traising of the cardinality of the universe. Part of Theorem
5.2 of [Specker] p. 973. (Contributed by
SF, 4Mar2015.)

⊢ T_{c}
Nc V = Nc
1_{c} 

Theorem  tcnc1c 6227 
Compute the Traising of the cardinality of one. Part of Theorem 5.2 of
[Specker] p. 973. (Contributed by SF,
4Mar2015.)

⊢ T_{c}
Nc 1_{c} = Nc ℘_{1}1_{c} 

Theorem  tc11 6228 
Cardinal T is onetoone. Based on theorem 2.4 of [Specker] p. 972.
(Contributed by SF, 10Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ NC ) → ( T_{c} M =
T_{c} N ↔ M =
N)) 

Theorem  taddc 6229* 
T raising rule for cardinal sum. (Contributed by SF, 11Mar2015.)

⊢ (((A ∈ NC ∧ B ∈ NC ∧ X ∈ NC ) ∧ T_{c}
A = ( T_{c} B
+_{c} X)) → ∃c ∈ NC X = T_{c}
c) 

Theorem  tlecg 6230 
Traising perserves order for cardinals. Theorem 5.5 of [Specker]
p. 973. (Contributed by SF, 11Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M ≤_{c} N ↔ T_{c}
M ≤_{c} T_{c} N)) 

Theorem  letc 6231* 
If a cardinal is less than or equal to a Traising, then it is also a
Traising. Theorem 5.6 of [Specker] p.
973. (Contributed by SF,
11Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ NC ∧ M
≤_{c} T_{c} N) → ∃p ∈ NC M = T_{c}
p) 

Theorem  ce0t 6232* 
If (M ↑_{c}
0_{c}) is a cardinal, then M is a Traising of some
cardinal. (Contributed by SF, 17Mar2015.)

⊢ ((M ∈ NC ∧ (M
↑_{c} 0_{c}) ∈ NC ) → ∃n ∈ NC M = T_{c}
n) 

Theorem  ce2le 6233 
Partial ordering law for base two cardinal exponentiation. Theorem 4.8
of [Specker] p. 973. (Contributed by
SF, 16Mar2015.)

⊢ (((M ∈ NC ∧ N ∈ NC ∧ (N
↑_{c} 0_{c}) ∈ NC ) ∧ M
≤_{c} N) →
(2_{c} ↑_{c} M) ≤_{c} (2_{c}
↑_{c} N)) 

Theorem  cet 6234 
The exponent of a Traising to a Traising is always a cardinal.
(Contributed by SF, 13Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ NC ) → ( T_{c} M
↑_{c} T_{c} N) ∈ NC ) 

Theorem  ce2t 6235 
The exponent of two to a Traising is always a cardinal. Theorem 5.8 of
[Specker] p. 973. (Contributed by SF,
13Mar2015.)

⊢ (M ∈ NC →
(2_{c} ↑_{c} T_{c} M)
∈ NC
) 

Theorem  tce2 6236 
Distributive law for Traising and cardinal exponentiation to two.
(Contributed by SF, 13Mar2015.)

⊢ ((M ∈ NC ∧ (M
↑_{c} 0_{c}) ∈ NC ) → T_{c} (2_{c}
↑_{c} M) =
(2_{c} ↑_{c} T_{c} M)) 

Theorem  te0c 6237 
A Traising raised to zero is always a cardinal. (Contributed by SF,
16Mar2015.)

⊢ (M ∈ NC → ( T_{c} M
↑_{c} 0_{c}) ∈ NC
) 

Theorem  ce0tb 6238* 
(M ↑_{c}
0_{c}) is a cardinal iff M is a Traising of some cardinal.
(Contributed by SF, 17Mar2015.)

⊢ (M ∈ NC →
((M ↑_{c}
0_{c}) ∈ NC ↔ ∃n ∈ NC M = T_{c} 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, 18Mar2015.)

⊢ (M ∈ NC →
((M ↑_{c}
0_{c}) ∈ NC ↔ M
≤_{c} Nc
1_{c})) 

Theorem  tlenc1c 6240 
A Traising is less than or equal to the cardinality of cardinal one.
(Contributed by SF, 16Mar2015.)

⊢ (M ∈ NC → T_{c} M
≤_{c} Nc
1_{c}) 

Theorem  1ne0c 6241 
Cardinal one is not zero. (Contributed by SF, 4Mar2015.)

⊢ 1_{c} ≠
0_{c} 

Theorem  2ne0c 6242 
Cardinal two is not zero. (Contributed by SF, 4Mar2015.)

⊢ 2_{c} ≠
0_{c} 

Theorem  finnc 6243 
A set is finite iff its cardinality is a natural. (Contributed by SF,
18Mar2015.)

⊢ (A ∈ Fin ↔ Nc A ∈ Nn
) 

Theorem  tcfnex 6244 
The stratified T raising function is a set. (Contributed by SF,
18Mar2015.)

⊢ TcFn ∈
V 

Theorem  fntcfn 6245 
Functionhood statement for the stratified Traising function.
(Contributed by SF, 18Mar2015.)

⊢ TcFn Fn 1_{c} 

Theorem  brtcfn 6246 
Binary relationship form of the stratified Traising function.
(Contributed by SF, 18Mar2015.)

⊢ A ∈ V ⇒ ⊢ ({A}TcFnB ↔
B = T_{c} A) 

Theorem  ncfin 6247 
The cardinality of a set is a natural iff the set is finite.
(Contributed by SF, 19Mar2015.)

⊢ A ∈ V ⇒ ⊢ ( Nc A ∈ Nn ↔ A ∈ Fin
) 

Theorem  nclennlem1 6248* 
Lemma for nclenn 6249. Set up stratification for induction.
(Contributed
by SF, 19Mar2015.)

⊢ {x ∣ ∀n ∈ NC (n
≤_{c} x → n ∈ Nn )} ∈
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, 19Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ Nn ∧ M
≤_{c} N) → M ∈ Nn ) 

Theorem  addcdi 6250 
Distributivity law for cardinal addition and multiplication. Theorem
XI.2.31 of [Rosser] p. 379. (Contributed
by Scott Fenton,
31Jul2019.)

⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) →
(A ·_{c} (B +_{c} C)) = ((A
·_{c} B)
+_{c} (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,
31Jul2019.)

⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) →
((A +_{c} B) ·_{c} C) = ((A
·_{c} C)
+_{c} (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, 31Jul2019.)

⊢ ((A ∈ NC ∧ B ∈ NC ) →
((A ·_{c} B) = 0_{c} ↔ (A = 0_{c}
∨ B =
0_{c}))) 

Theorem  lemuc1 6253 
Multiplication law for cardinal less than. Theorem XI.2.35 of [Rosser]
p. 380. (Contributed by Scott Fenton, 31Jul2019.)

⊢ (((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) ∧ A
≤_{c} B) → (A ·_{c} C) ≤_{c} (B ·_{c} C)) 

Theorem  lemuc2 6254 
Multiplication law for cardinal less than. (Contributed by Scott Fenton,
31Jul2019.)

⊢ (((A ∈ NC ∧ B ∈ NC ∧ C ∈ 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,
31Jul2019.)

⊢ ((M ∈ NC ∧ N ∈ NC ∧ N ≠
0_{c}) → 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, 31Jul2019.)

⊢ ( 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,
31Jul2019.)

⊢ (V × V) ≈ V 

Theorem  0lt1c 6258 
Cardinal one is strictly greater than cardinal zero. (Contributed by
Scott Fenton, 1Aug2019.)

⊢ 0_{c} <_{c}
1_{c} 

Theorem  csucex 6259 
The function mapping x to its
cardinal successor exists.
(Contributed by Scott Fenton, 30Jul2019.)

⊢ (x ∈ V ↦ (x +_{c} 1_{c})) ∈ V 

Theorem  brcsuc 6260* 
Binary relationship form of the successor mapping function.
(Contributed by Scott Fenton, 2Aug2019.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A(x ∈ V ↦ (x
+_{c} 1_{c}))B ↔ B =
(A +_{c}
1_{c})) 

Theorem  nnltp1clem1 6261 
Lemma for nnltp1c 6262. Set up stratification. (Contributed by SF,
25Mar2015.)

⊢ {x ∣ x
<_{c} (x +_{c}
1_{c})} ∈ V 

Theorem  nnltp1c 6262 
Any natural is less than one plus itself. (Contributed by SF,
25Mar2015.)

⊢ (N ∈ Nn → N <_{c} (N +_{c}
1_{c})) 

Theorem  addccan2nclem1 6263* 
Lemma for addccan2nc 6265. Stratification helper theorem.
(Contributed
by Scott Fenton, 2Aug2019.)

⊢ (x( AddC ∘ ^{◡}(1^{st} ↾ (V × {n})))y ↔
y = (x
+_{c} n)) 

Theorem  addccan2nclem2 6264* 
Lemma for addccan2nc 6265. Establish stratification for induction.
(Contributed by Scott Fenton, 2Aug2019.)

⊢ ((N ∈ V ∧ P ∈ W) →
{x ∣
((x +_{c} N) = (x
+_{c} P) → N = P)} ∈ 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, 2Aug2019.)

⊢ ((M ∈ Nn ∧ N ∈ NC ∧ P ∈ NC ) →
((M +_{c} N) = (M
+_{c} 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, 2Aug2019.)

⊢ ((M ∈ Nn ∧ N ∈ NC ∧ P ∈ NC ) →
((M +_{c} N) ≤_{c} (M +_{c} P) ↔ N
≤_{c} P)) 

Theorem  ncslesuc 6267 
Relationship between successor and cardinal less than or equal.
(Contributed by Scott Fenton, 3Aug2019.)

⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M ≤_{c} (N +_{c} 1_{c}) ↔
(M ≤_{c} N ∨ M = (N
+_{c} 1_{c})))) 

Theorem  nmembers1lem1 6268* 
Lemma for nmembers1 6271. Set up stratification. (Contributed by SF,
25Mar2015.)

⊢ {x ∣ {m ∈ Nn ∣ (1_{c} ≤_{c} m ∧ m ≤_{c} x)} ∈ T_{c} T_{c} x}
∈ V 

Theorem  nmembers1lem2 6269 
Lemma for nmembers1 6271. The set of all elements between one and
zero is
empty. (Contributed by Scott Fenton, 1Aug2019.)

⊢ {m ∈ Nn ∣ (1_{c} ≤_{c} m ∧ m ≤_{c} 0_{c})} ∈ 0_{c} 

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, 3Aug2019.)

⊢ ((A ∈ Nn ∧ B ∈ Nn ) →
({m ∈
Nn ∣
(1_{c} ≤_{c} m
∧ m
≤_{c} A)} ∈ B →
{m ∈
Nn ∣
(1_{c} ≤_{c} m
∧ m
≤_{c} (A +_{c}
1_{c}))} ∈ (B +_{c}
1_{c}))) 

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 ∈ Nn ∣ (1_{c} ≤_{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,
3Aug2019.)

⊢ (N ∈ Nn → {m ∈ Nn ∣
(1_{c} ≤_{c} m
∧ m
≤_{c} N)} ∈ T_{c} T_{c} N) 

Theorem  ltcirr 6272 
Cardinal less than is irreflexive. (Contributed by Scott Fenton,
12Dec2021.)

⊢ ¬ 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
Sp_{ac} 

Definition  dfspac 6274* 
Define the special class generator for the disproof of the axiom of
choice. Definition 6.1 of [Specker] p.
973. (Contributed by SF,
3Mar2015.)

⊢ Sp_{ac} =
(m ∈
NC ↦ Clos1 ({m}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2_{c} ↑_{c} x))})) 

Theorem  nncdiv3lem1 6275 
Lemma for nncdiv3 6277. Set up a helper for stratification.
(Contributed
by SF, 3Mar2015.)

⊢ (⟨n, b⟩ ∈ ran ( Ins3 ^{◡}((ran
(^{◡}1^{st} ⊗
(1^{st} ∩ 2^{nd} )) ⊗ 2^{nd} ) “
AddC ) ∩ (((1^{st} ∘ 1^{st} ) ⊗ ((2^{nd}
∘ 1^{st} ) ⊗ 2^{nd}
)) “ AddC )) ↔ b = ((n
+_{c} n)
+_{c} n)) 

Theorem  nncdiv3lem2 6276* 
Lemma for nncdiv3 6277. Set up stratification for induction.
(Contributed by SF, 2Mar2015.)

⊢ {a ∣ ∃n ∈ Nn (a = ((n +_{c} n) +_{c} n) ∨ a = (((n
+_{c} n)
+_{c} n)
+_{c} 1_{c}) ∨
a = (((n +_{c} n) +_{c} n) +_{c} 2_{c}))}
∈ V 

Theorem  nncdiv3 6277* 
Divisibility by three rule for finite cardinals. Part of Theorem 3.4 of
[Specker] p. 973. (Contributed by SF,
2Mar2015.)

⊢ (A ∈ Nn → ∃n ∈ Nn (A = ((n
+_{c} n)
+_{c} n) ∨ A =
(((n +_{c} n) +_{c} n) +_{c} 1_{c}) ∨ A =
(((n +_{c} n) +_{c} n) +_{c}
2_{c}))) 

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,
13Mar2015.)

⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬
((A +_{c} A) +_{c} A) = (((B
+_{c} B)
+_{c} B)
+_{c} 1_{c})) 

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,
12Mar2015.)

⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬
((A +_{c} A) +_{c} A) = (((B
+_{c} B)
+_{c} B)
+_{c} 2_{c})) 

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, 12Mar2015.)

⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬
(((A +_{c} A) +_{c} A) +_{c} 1_{c}) =
(((B +_{c} B) +_{c} B) +_{c}
2_{c})) 

Theorem  spacvallem1 6281* 
Lemma for spacval 6282. Set up stratification for the recursive
relationship. (Contributed by SF, 6Mar2015.)

⊢ {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_{c} ↑_{c}
x))} ∈
V 

Theorem  spacval 6282* 
The value of the special set generator. (Contributed by SF,
4Mar2015.)

⊢ (N ∈ NC → ( Sp_{ac} ‘N) = Clos1 ({N}, {⟨x, y⟩ ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2_{c} ↑_{c}
x))})) 

Theorem  fnspac 6283 
The special set generator is a function over the cardinals.
(Contributed by SF, 18Mar2015.)

⊢ Sp_{ac}
Fn NC 

Theorem  spacssnc 6284 
The special set generator generates a set of cardinals. (Contributed by
SF, 13Mar2015.)

⊢ (N ∈ NC → ( Sp_{ac} ‘N) ⊆ NC ) 

Theorem  spacid 6285 
The initial value of the special set generator is an element.
(Contributed by SF, 13Mar2015.)

⊢ (M ∈ NC → M ∈ ( Sp_{ac} ‘M)) 

Theorem  spaccl 6286 
Closure law for the special set generator. (Contributed by SF,
13Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ ( Sp_{ac}
‘M) ∧ (N
↑_{c} 0_{c}) ∈ NC ) →
(2_{c} ↑_{c} N) ∈ ( Sp_{ac} ‘M)) 

Theorem  spacind 6287* 
Inductive law for the special set generator. (Contributed by SF,
13Mar2015.)

⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Sp_{ac} ‘M)((x ∈ S ∧ (x
↑_{c} 0_{c}) ∈ NC ) →
(2_{c} ↑_{c} x) ∈ S))) → ( Sp_{ac} ‘M) ⊆ S) 

Theorem  spacis 6288* 
Induction scheme for the special set generator. (Contributed by SF,
13Mar2015.)

⊢ {x ∣ φ}
∈ V
& ⊢ (x =
M → (φ ↔ ψ))
& ⊢ (x =
y → (φ ↔ χ))
& ⊢ (x =
(2_{c} ↑_{c} y) → (φ ↔ θ))
& ⊢ (x =
N → (φ ↔ τ))
& ⊢ (M ∈ NC → ψ)
& ⊢ (((M ∈ NC ∧ y ∈ ( Sp_{ac}
‘M)) ∧ ((y
↑_{c} 0_{c}) ∈ NC ∧ χ))
→ θ)
⇒ ⊢ ((M ∈ NC ∧ N ∈ ( Sp_{ac} ‘M)) → τ) 

Theorem  nchoicelem1 6289 
Lemma for nchoice 6308. A finite cardinal is not one more than its
Traising. (Contributed by SF, 3Mar2015.)

⊢ (A ∈ Nn → ¬
A = ( T_{c} A
+_{c} 1_{c})) 

Theorem  nchoicelem2 6290 
Lemma for nchoice 6308. A finite cardinal is not two more than its
Traising. (Contributed by SF, 12Mar2015.)

⊢ (A ∈ Nn → ¬
A = ( T_{c} A
+_{c} 2_{c})) 

Theorem  nchoicelem3 6291 
Lemma for nchoice 6308. Compute the value of Sp_{ac} when the argument
is not exponentiable. Theorem 6.2 of [Specker] p. 973. (Contributed by
SF, 13Mar2015.)

⊢ ((M ∈ NC ∧ ¬ (M
↑_{c} 0_{c}) ∈ NC ) → ( Sp_{ac} ‘M) = {M}) 

Theorem  nchoicelem4 6292 
Lemma for nchoice 6308. The initial value of Sp_{ac} is a minimum
value. Theorem 6.4 of [Specker] p. 973.
(Contributed by SF,
13Mar2015.)

⊢ ((M ∈ NC ∧ N ∈ ( Sp_{ac}
‘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, 13Mar2015.)

⊢ ((M ∈ NC ∧ (M
↑_{c} 0_{c}) ∈ NC ) → ¬
M ∈ (
Sp_{ac} ‘(2_{c}
↑_{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,
13Mar2015.)

⊢ ((M ∈ NC ∧ (M
↑_{c} 0_{c}) ∈ NC ) → ( Sp_{ac} ‘M) = ({M} ∪
( Sp_{ac} ‘(2_{c}
↑_{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,
13Mar2015.)

⊢ ((M ∈ NC ∧ (M
↑_{c} 0_{c}) ∈ NC ) → Nc ( Sp_{ac}
‘M) = ( Nc ( Sp_{ac}
‘(2_{c} ↑_{c} M)) +_{c}
1_{c})) 

Theorem  nchoicelem8 6296 
Lemma for nchoice 6308. An anticlosure condition for cardinal
exponentiation to zero. Theorem 4.5 of [Specker] p. 973. (Contributed by
SF, 18Mar2015.)

⊢ (( ≤_{c} We NC ∧ M ∈ NC ) → (¬
(M ↑_{c}
0_{c}) ∈ NC ↔ Nc
1_{c} <_{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, 18Mar2015.)

⊢ (( ≤_{c} We NC ∧ M ∈ NC ∧ ¬ (M
↑_{c} 0_{c}) ∈ NC ) → ( Nc ( Sp_{ac}
‘ T_{c} M) = 2_{c}
∨ Nc ( Sp_{ac} ‘ T_{c} M) =
3_{c})) 

Theorem  nchoicelem10 6298 
Lemma for nchoice 6308. Stratification helper lemma. (Contributed
by SF,
18Mar2015.)

⊢ S ∈ V
& ⊢ X ∈ V ⇒ ⊢ (⟨c, X⟩ ∈ ∼ ((
Ins3 S ⊕
Ins2 ∼ ran (^{◡} ∼ S
⊗ (^{◡} S
↾ Fix
( S ∘
ImageS)))) “ 1_{c})
↔ c = Clos1
(X, S)) 

Theorem  nchoicelem11 6299* 
Lemma for nchoice 6308. Set up stratification for nchoicelem12 6300.
(Contributed by SF, 18Mar2015.)

⊢ {t ∣ ∀m ∈ NC (t = Nc ( Sp_{ac}
‘ T_{c} m) → Nc ( Sp_{ac} ‘m) ∈ Nn )} ∈
V 

Theorem  nchoicelem12 6300 
Lemma for nchoice 6308. If the Traising of a cardinal yields a
finite
special set, then so does the initial set. Theorem 7.1 of [Specker]
p. 974. (Contributed by SF, 18Mar2015.)

⊢ ((M ∈ NC ∧ ( Sp_{ac}
‘ T_{c} M) ∈ Fin ) → ( Sp_{ac} ‘M) ∈ Fin ) 