Type  Label  Description 
Statement 

Definition  dfnc 6101 
Define the cardinality operation. This is the unique cardinal number
containing a given set. Definition from [Rosser] p. 371. (Contributed by
Scott Fenton, 24Feb2015.)

Nc 

Definition  dfmuc 6102* 
Define cardinal multiplication. Definition from [Rosser] p. 378.
(Contributed by Scott Fenton, 24Feb2015.)

·_{c}
NC NC 

Definition  dftc 6103* 
Define the typeraising operation on a cardinal number. This is the
unique cardinal containing the unit power classes of the elements of the
given cardinal. Definition adapted from [Rosser] p. 528. (Contributed
by Scott Fenton, 24Feb2015.)

T_{c}
NC
Nc _{1} 

Definition  df2c 6104 
Define cardinal two. This is the set of all sets with two unique
elements. (Contributed by Scott Fenton, 24Feb2015.)

2_{c} Nc 

Definition  df3c 6105 
Define cardinal three. This is the set of all sets with three unique
elements. (Contributed by Scott Fenton, 24Feb2015.)

3_{c} Nc 

Definition  dfce 6106* 
Define cardinal exponentiation. Definition from [Rosser] p. 381.
(Contributed by Scott Fenton, 24Feb2015.)

↑_{c}
NC NC _{1} _{1} 

Definition  dftcfn 6107 
Define the stratified Traising function. (Contributed by Scott Fenton,
24Feb2015.)

TcFn 1_{c}
T_{c} 

Theorem  nceq 6108 
Cardinality equality law. (Contributed by SF, 24Feb2015.)

Nc Nc 

Theorem  nceqi 6109 
Equality inference for cardinality. (Contributed by SF,
24Feb2015.)

Nc Nc 

Theorem  nceqd 6110 
Equality deduction for cardinality. (Contributed by SF,
24Feb2015.)

Nc Nc 

Theorem  ncsex 6111 
The class of all cardinal numbers is a set. (Contributed by SF,
24Feb2015.)

NC 

Theorem  brlecg 6112* 
Binary relationship form of cardinal less than or equal. (Contributed
by SF, 24Feb2015.)

_{c}


Theorem  brlec 6113* 
Binary relationship form of cardinal less than or equal. (Contributed
by SF, 24Feb2015.)

_{c}


Theorem  brltc 6114 
Binary relationship form of cardinal less than. (Contributed by SF,
4Mar2015.)

_{c} _{c} 

Theorem  lecex 6115 
Cardinal less than or equal is a set. (Contributed by SF,
24Feb2015.)

_{c} 

Theorem  ltcex 6116 
Cardinal strict less than is a set. (Contributed by SF, 24Feb2015.)

_{c} 

Theorem  ncex 6117 
The cardinality of a class is a set. (Contributed by SF, 24Feb2015.)

Nc 

Theorem  nulnnc 6118 
The empty class is not a cardinal number. (Contributed by SF,
24Feb2015.)

NC 

Theorem  elncs 6119* 
Membership in the cardinals. (Contributed by SF, 24Feb2015.)

NC
Nc 

Theorem  ncelncs 6120 
The cardinality of a set is a cardinal number. (Contributed by SF,
24Feb2015.)

Nc NC 

Theorem  ncelncsi 6121 
The cardinality of a set is a cardinal number. (Contributed by SF,
10Mar2015.)

Nc NC 

Theorem  ncidg 6122 
A set is a member of its own cardinal. (Contributed by SF,
24Feb2015.)

Nc 

Theorem  ncid 6123 
A set is a member of its own cardinal. (Contributed by SF,
24Feb2015.)

Nc 

Theorem  ncprc 6124 
The cardinality of a proper class is the empty set. (Contributed by SF,
24Feb2015.)

Nc 

Theorem  elnc 6125 
Membership in cardinality. (Contributed by SF, 24Feb2015.)

Nc 

Theorem  eqncg 6126 
Equality of cardinalities. (Contributed by SF, 24Feb2015.)

Nc Nc 

Theorem  eqnc 6127 
Equality of cardinalities. (Contributed by SF, 24Feb2015.)

Nc Nc 

Theorem  ncseqnc 6128 
A cardinal is equal to the cardinality of a set iff it contains the set.
(Contributed by SF, 24Feb2015.)

NC Nc 

Theorem  eqnc2 6129 
Alternate condition for equality to a cardinality. (Contributed by SF,
18Mar2015.)

Nc NC 

Theorem  ovmuc 6130* 
The value of cardinal multiplication. (Contributed by SF,
10Mar2015.)

NC NC
·_{c} 

Theorem  mucnc 6131 
Cardinal multiplication in terms of cardinality. Theorem XI.2.27 of
[Rosser] p. 378. (Contributed by SF,
10Mar2015.)

Nc ·_{c} Nc Nc 

Theorem  muccl 6132 
Closure law for cardinal multiplication. (Contributed by SF,
10Mar2015.)

NC NC
·_{c} NC 

Theorem  mucex 6133 
Cardinal multiplication is a set. (Contributed by SF, 24Feb2015.)

·_{c} 

Theorem  muccom 6134 
Cardinal multiplication commutes. Theorem XI.2.28 of [Rosser] p. 378.
(Contributed by SF, 10Mar2015.)

NC NC
·_{c} ·_{c} 

Theorem  mucass 6135 
Cardinal multiplication associates. Theorem XI.2.29 of [Rosser] p. 378.
(Contributed by SF, 10Mar2015.)

NC NC NC ·_{c} ·_{c} ·_{c} ·_{c} 

Theorem  ncdisjun 6136 
Cardinality of disjoint union of two sets. (Contributed by SF,
24Feb2015.)

Nc
Nc Nc 

Theorem  df0c2 6137 
Cardinal zero is the cardinality of the empty set. Theorem XI.2.7 of
[Rosser] p. 372. (Contributed by SF,
24Feb2015.)

0_{c} Nc 

Theorem  0cnc 6138 
Cardinal zero is a cardinal number. Corollary 1 to theorem XI.2.7 of
[Rosser] p. 373. (Contributed by SF,
24Feb2015.)

0_{c} NC 

Theorem  1cnc 6139 
Cardinal one is a cardinal number. Corollary 2 to theorem XI.2.8 of
[Rosser] p. 373. (Contributed by SF,
24Feb2015.)

1_{c} NC 

Theorem  df1c3 6140 
Cardinal one is the cardinality of a singleton. Theorem XI.2.8 of
[Rosser] p. 373. (Contributed by SF,
2Mar2015.)

1_{c} Nc 

Theorem  df1c3g 6141 
Cardinal one is the cardinality of a singleton. Theorem XI.2.8 of
[Rosser] p. 373. (Contributed by SF,
13Mar2015.)

1_{c} Nc 

Theorem  muc0 6142 
Cardinal multiplication by zero. Theorem XI.2.32 of [Rosser] p. 379.
(Contributed by SF, 10Mar2015.)

NC
·_{c} 0_{c} 0_{c} 

Theorem  mucid1 6143 
Cardinal multiplication by one. (Contributed by SF, 11Mar2015.)

NC
·_{c} 1_{c} 

Theorem  ncaddccl 6144 
The cardinals are closed under cardinal addition. Theorem XI.2.10 of
[Rosser] p. 374. (Contributed by SF,
24Feb2015.)

NC NC NC 

Theorem  peano2nc 6145 
The successor of a cardinal is a cardinal. (Contributed by SF,
24Feb2015.)

NC 1_{c} NC 

Theorem  nnnc 6146 
A finite cardinal number is a cardinal number. (Contributed by SF,
24Feb2015.)

Nn NC 

Theorem  nnssnc 6147 
The finite cardinals are a subset of the cardinals. Theorem XI.2.11 of
[Rosser] p. 374. (Contributed by SF,
24Feb2015.)

Nn NC 

Theorem  ncdisjeq 6148 
Two cardinals are either disjoint or equal. (Contributed by SF,
25Feb2015.)

NC NC 

Theorem  nceleq 6149 
If two cardinals have an element in common, then they are equal.
(Contributed by SF, 25Feb2015.)

NC NC


Theorem  peano4nc 6150 
Successor is onetoone over the cardinals. Theorem XI.2.12 of [Rosser]
p. 375. (Contributed by SF, 25Feb2015.)

NC NC 1_{c}
1_{c}


Theorem  ncssfin 6151 
A cardinal is finite iff it is a subset of Fin.
(Contributed by
SF, 25Feb2015.)

NC Nn Fin 

Theorem  ncpw1 6152 
The cardinality of two sets are equal iff their unit power classes have
the same cardinality. (Contributed by SF, 25Feb2015.)

Nc Nc Nc _{1} Nc _{1} 

Theorem  ncpwpw1 6153 
Power class and unit power class commute within cardinality.
(Contributed by SF, 26Feb2015.)

Nc _{1} Nc _{1} 

Theorem  ncpw1c 6154 
The cardinality of 1_{c} is equal to that of its power class.
(Contributed by SF, 26Feb2015.)

Nc 1_{c}
Nc 1_{c} 

Theorem  1p1e2c 6155 
One plus one equals two. Theorem *110.64 of [WhiteheadRussell] p. 86.
This theorem is occasionally useful. (Contributed by SF, 2Mar2015.)

1_{c} 1_{c}
2_{c} 

Theorem  2p1e3c 6156 
Two plus one equals three. (Contributed by SF, 2Mar2015.)

2_{c} 1_{c}
3_{c} 

Theorem  tcex 6157 
The cardinal T operation always yields a set. (Contributed by SF,
2Mar2015.)

T_{c}


Theorem  tceq 6158 
Equality theorem for cardinal T operator. (Contributed by SF,
2Mar2015.)

T_{c} T_{c} 

Theorem  ncspw1eu 6159* 
Given a cardinal, there is a unique cardinal that contains the unit
power class of its members. (Contributed by SF, 2Mar2015.)

NC NC Nc _{1} 

Theorem  tccl 6160 
The cardinal T operation over a cardinal yields a cardinal.
(Contributed by SF, 2Mar2015.)

NC T_{c} NC 

Theorem  eqtc 6161* 
The defining property of the cardinal T operation. (Contributed by SF,
2Mar2015.)

NC T_{c}
Nc _{1} 

Theorem  pw1eltc 6162 
The unit power class of an element of a cardinal is in the cardinal's T
raising. (Contributed by SF, 2Mar2015.)

NC _{1} T_{c} 

Theorem  tc0c 6163 
The T raising of cardinal zero is still cardinal zero. (Contributed by
SF, 2Mar2015.)

T_{c}
0_{c}
0_{c} 

Theorem  tcdi 6164 
T raising distributes over addition. (Contributed by SF,
2Mar2015.)

NC NC T_{c} T_{c} T_{c} 

Theorem  tc1c 6165 
T raising does not change cardinal one. (Contributed by SF,
2Mar2015.)

T_{c}
1_{c}
1_{c} 

Theorem  tc2c 6166 
T raising does not change cardinal two. (Contributed by SF,
2Mar2015.)

T_{c}
2_{c}
2_{c} 

Theorem  2nnc 6167 
Two is a finite cardinal. (Contributed by SF, 4Mar2015.)

2_{c} Nn 

Theorem  2nc 6168 
Two is a cardinal number. (Contributed by SF, 3Mar2015.)

2_{c} NC 

Theorem  pw1fin 6169 
The unit power class of a finite set is finite. (Contributed by SF,
3Mar2015.)

Fin _{1} Fin 

Theorem  nntccl 6170 
Cardinal T is closed under the natural numbers. (Contributed by SF,
3Mar2015.)

Nn T_{c} Nn 

Theorem  ovcelem1 6171* 
Lemma for ovce 6172. Set up stratification for the result.
(Contributed
by SF, 6Mar2015.)

_{1} _{1} 

Theorem  ovce 6172* 
The value of cardinal exponentiation. (Contributed by SF,
3Mar2015.)

NC NC
↑_{c} _{1} _{1} 

Theorem  ceexlem1 6173* 
Lemma for ceex 6174. Set up part of the stratification.
(Contributed by
SF, 6Mar2015.)

S SI Pw1Fn _{1} 

Theorem  ceex 6174 
Cardinal exponentiation is stratified. (Contributed by SF,
3Mar2015.)

↑_{c} 

Theorem  elce 6175* 
Membership in cardinal exponentiation. Theorem XI.2.38 of [Rosser]
p. 382. (Contributed by SF, 6Mar2015.)

NC NC ↑_{c} _{1} _{1} 

Theorem  fnce 6176 
Functionhood statement for cardinal exponentiation. (Contributed by SF,
6Mar2015.)

↑_{c} NC NC 

Theorem  ce0nnul 6177* 
A condition for cardinal exponentiation being nonempty. Theorem XI.2.42
of [Rosser] p. 382. (Contributed by SF,
6Mar2015.)

NC ↑_{c}
0_{c}
_{1} 

Theorem  ce0nnuli 6178 
Inference form of ce0nnul 6177. (Contributed by SF, 9Mar2015.)

NC _{1} ↑_{c} 0_{c} 

Theorem  ce0addcnnul 6179 
The sum of two cardinals raised to 0_{c} is nonempty iff each
addend
raised to 0_{c} is nonempty. Theorem XI.2.43 of [Rosser] p. 383.
(Contributed by SF, 9Mar2015.)

NC NC
↑_{c} 0_{c}
↑_{c} 0_{c}
↑_{c} 0_{c} 

Theorem  ce0nn 6180 
A natural raised to cardinal zero is nonempty. Theorem XI.2.44 of
[Rosser] p. 383. (Contributed by SF,
9Mar2015.)

Nn
↑_{c} 0_{c} 

Theorem  cenc 6181 
Cardinal exponentiation in terms of cardinality. Theorem XI.2.39 of
[Rosser] p. 382. (Contributed by SF,
6Mar2015.)

Nc _{1} ↑_{c} Nc
_{1} Nc


Theorem  ce0nnulb 6182 
Cardinal exponentiation is nonempty iff the two sets raised to zero are
nonempty. Theorem XI.2.47 of [Rosser] p.
384. (Contributed by SF,
9Mar2015.)

NC NC ↑_{c}
0_{c}
↑_{c} 0_{c}
↑_{c} 

Theorem  ceclb 6183 
Biconditional closure law for cardinal exponentiation. Theorem XI.2.48
of [Rosser] p. 384. (Contributed by SF,
9Mar2015.)

NC NC ↑_{c}
0_{c}
↑_{c} 0_{c}
↑_{c} NC 

Theorem  ce0nulnc 6184 
Cardinal exponentiation to zero is a cardinal iff it is nonempty.
Corollary 1 of theorem XI.2.38 of [Rosser]
p. 384. (Contributed by SF,
13Mar2015.)

NC ↑_{c}
0_{c}
↑_{c}
0_{c}
NC 

Theorem  ce0ncpw1 6185* 
If cardinal exponentiation to zero is a cardinal, then the base is the
cardinality of some unit power class. Corollary 2 of theorem XI.2.48 of
[Rosser] p. 384. (Contributed by SF,
9Mar2015.)

NC ↑_{c} 0_{c} NC
Nc _{1} 

Theorem  cecl 6186 
Closure law for cardinal exponentiation. Corollary 3 of theorem XI.2.48
of [Rosser] p. 384. (Contributed by SF,
9Mar2015.)

NC NC ↑_{c}
0_{c}
NC
↑_{c} 0_{c} NC
↑_{c} NC 

Theorem  ceclr 6187 
Reverse closure law for cardinal exponentiation. (Contributed by SF,
13Mar2015.)

NC NC
↑_{c} NC ↑_{c} 0_{c} NC
↑_{c} 0_{c} NC 

Theorem  fce 6188 
Full functionhood statement for cardinal exponentiation. (Contributed
by SF, 13Mar2015.)

↑_{c} NC NC NC 

Theorem  ceclnn1 6189 
Closure law for cardinal exponentiation when the base is a natural.
(Contributed by SF, 13Mar2015.)

Nn NC
↑_{c} 0_{c} NC
↑_{c} NC 

Theorem  ce0 6190 
The value of nonempty cardinal exponentiation. Theorem XI.2.49 of
[Rosser] p. 385. (Contributed by SF,
9Mar2015.)

NC ↑_{c} 0_{c} NC
↑_{c} 0_{c} 1_{c} 

Theorem  el2c 6191* 
Membership in cardinal two. (Contributed by SF, 3Mar2015.)

2_{c}


Theorem  ce2 6192 
The value of base two cardinal exponentiation. Theorem XI.2.70 of
[Rosser] p. 389. (Contributed by SF,
3Mar2015.)

Nc _{1} 2_{c}
↑_{c} Nc 

Theorem  ce2nc1 6193 
Compute an exponent of the cardinality of one. Theorem 4.3 of [Specker]
p. 973. (Contributed by SF, 4Mar2015.)

2_{c} ↑_{c} Nc 1_{c} Nc 

Theorem  ce2ncpw11c 6194 
Compute an exponent of the cardinality of the unit power class of one.
Theorem 4.4 of [Specker] p. 973.
(Contributed by SF, 4Mar2015.)

2_{c} ↑_{c} Nc _{1} 1_{c}
Nc 1_{c} 

Theorem  nclec 6195 
A relationship between cardinality, subset, and cardinal less than.
(Contributed by SF, 17Mar2015.)

Nc _{c} Nc 

Theorem  lecidg 6196 
A nonempty set is less than or equal to itself. Theorem XI.2.14 of
[Rosser] p. 375. (Contributed by SF,
4Mar2015.)

_{c} 

Theorem  nclecid 6197 
A cardinal is less than or equal to itself. Corollary 1 of theorem
XI.2.14 of [Rosser] p. 376. (Contributed
by SF, 4Mar2015.)

NC _{c} 

Theorem  lec0cg 6198 
Cardinal zero is a minimal element of cardinal less than or equal.
Theorem XI.2.15 of [Rosser] p. 376.
(Contributed by SF, 4Mar2015.)

0_{c} _{c} 

Theorem  lecncvg 6199 
The cardinality of
is a maximal element of cardinal less than or
equal. Theorem XI.2.16 of [Rosser] p.
376. (Contributed by SF,
4Mar2015.)

_{c} Nc 

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

NC 0_{c} _{c} 