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 A = [A]
≈ 

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

⊢ ·_{c} = (m ∈ NC , n ∈ NC ↦ {a ∣ ∃b ∈ m ∃g ∈ n a ≈
(b × g)}) 

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}
A = (℩b(b ∈ NC ∧ ∃x ∈ A b = Nc ℘_{1}x)) 

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 {∅,
V} 

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 {∅, V, (V ∖ {∅})} 

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

⊢ ↑_{c} = (n ∈ NC , m ∈ NC ↦ {g ∣ ∃a∃b(℘_{1}a ∈ n ∧ ℘_{1}b ∈ m ∧ g ≈ (a
↑_{m} b))}) 

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

⊢ TcFn = (x
∈ 1_{c} ↦ T_{c}
∪x) 

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

⊢ (A =
B → Nc
A = Nc
B) 

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

⊢ A =
B ⇒ ⊢ Nc A = Nc B 

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

⊢ (φ
→ A = B) ⇒ ⊢ (φ
→ Nc A =
Nc B) 

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

⊢ NC ∈ V 

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

⊢ ((A ∈ V ∧ B ∈ W) →
(A ≤_{c} B ↔ ∃x ∈ A ∃y ∈ B x ⊆ y)) 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A
≤_{c} B ↔ ∃x ∈ A ∃y ∈ B x ⊆ y) 

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

⊢ (A
<_{c} B ↔ (A ≤_{c} B ∧ A ≠ B)) 

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

⊢ ≤_{c} ∈ V 

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

⊢ <_{c} ∈ V 

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

⊢ Nc A ∈
V 

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.)

⊢ (A ∈ NC ↔ ∃x A = Nc x) 

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

⊢ (A ∈ V →
Nc A ∈ NC
) 

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

⊢ A ∈ V ⇒ ⊢ Nc A ∈ NC 

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

⊢ (A ∈ V →
A ∈
Nc A) 

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

⊢ A ∈ V ⇒ ⊢ A ∈ Nc A 

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

⊢ (¬ A
∈ V → Nc
A = ∅) 

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

⊢ (A ∈ Nc B ↔ A
≈ B) 

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

⊢ (A ∈ V → (
Nc A = Nc B ↔
A ≈ B)) 

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

⊢ A ∈ V ⇒ ⊢ ( Nc A = Nc B ↔ A
≈ B) 

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

⊢ (A ∈ NC → (A = Nc X ↔ X
∈ A)) 

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

⊢ X ∈ V ⇒ ⊢ (A = Nc X ↔
(A ∈
NC ∧ X ∈ A)) 

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

⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M ·_{c} N) = {a ∣ ∃b ∈ M ∃g ∈ N a ≈
(b × g)}) 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ( Nc A ·_{c} Nc B) = Nc (A ×
B) 

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

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

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

⊢ ·_{c} ∈ V 

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

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

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

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

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ((A ∩
B) = ∅
→ Nc (A
∪ B) = ( Nc A
+_{c} Nc B)) 

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.)

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

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

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

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

⊢ (A ∈ NC → (A ·_{c} 0_{c})
= 0_{c}) 

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

⊢ (A ∈ NC → (A ·_{c} 1_{c})
= A) 

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

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

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

⊢ (A ∈ NC → (A +_{c} 1_{c}) ∈ NC
) 

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

⊢ (A ∈ Nn → A ∈ 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.)

⊢ ((A ∈ NC ∧ B ∈ NC ) →
((A ∩ B) = ∅ ∨ A = B)) 

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

⊢ (((A ∈ NC ∧ B ∈ NC ) ∧ (X ∈ A ∧ X ∈ B)) →
A = B) 

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

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

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

⊢ (A ∈ NC → (A ∈ Nn ↔ A ⊆ Fin
)) 

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

⊢ A ∈ V ⇒ ⊢ ( Nc A = Nc B ↔ Nc ℘_{1}A = Nc ℘_{1}B) 

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

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

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} +_{c}
1_{c}) = 2_{c} 

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

⊢ (2_{c} +_{c}
1_{c}) = 3_{c} 

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

⊢ T_{c}
A ∈
V 

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

⊢ (A =
B → T_{c} A =
T_{c} B) 

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

⊢ (A ∈ NC → ∃!x ∈ NC ∃y ∈ A x = Nc ℘_{1}y) 

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

⊢ (A ∈ NC → T_{c} A
∈ NC
) 

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

⊢ (A ∈ NC → ( T_{c} A =
B ↔ ∃x ∈ A B = Nc ℘_{1}x)) 

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

⊢ ((A ∈ NC ∧ B ∈ A) →
℘_{1}B ∈ T_{c} A) 

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.)

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

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.)

⊢ (A ∈ Fin → ℘_{1}A ∈ Fin ) 

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

⊢ (A ∈ Nn → T_{c} A
∈ Nn
) 

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

⊢ ((N ∈ V ∧ M ∈ W) →
{g ∣
∃a∃b(℘_{1}a ∈ N ∧ ℘_{1}b ∈ M ∧ g ≈ (a
↑_{m} b))} ∈ V) 

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

⊢ ((N ∈ NC ∧ M ∈ NC ) →
(N ↑_{c} M) = {g ∣ ∃a∃b(℘_{1}a ∈ N ∧ ℘_{1}b ∈ M ∧ g ≈ (a
↑_{m} b))}) 

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

⊢ (⟨{{a}}, n⟩ ∈ ( S ∘ SI Pw1Fn ) ↔ ℘_{1}a ∈ n) 

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

⊢ ↑_{c} ∈ V 

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

⊢ ((N ∈ NC ∧ M ∈ NC ) →
(A ∈
(N ↑_{c} M) ↔ ∃x∃y(℘_{1}x ∈ N ∧ ℘_{1}y ∈ M ∧ A ≈ (x
↑_{m} y)))) 

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

⊢ ↑_{c} Fn ( NC × NC
) 

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

⊢ (M ∈ NC →
((M ↑_{c}
0_{c}) ≠ ∅ ↔ ∃a℘_{1}a ∈ M)) 

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

⊢ ((M ∈ NC ∧ ℘_{1}A ∈ M) → (M
↑_{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.)

⊢ ((M ∈ NC ∧ N ∈ NC ) →
(((M +_{c} N) ↑_{c} 0_{c})
≠ ∅ ↔ ((M ↑_{c} 0_{c})
≠ ∅ ∧
(N ↑_{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.)

⊢ (N ∈ Nn → (N ↑_{c} 0_{c})
≠ ∅) 

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

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ( Nc ℘_{1}A ↑_{c} Nc ℘_{1}B) = Nc (A ↑_{m} B) 

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.)

⊢ ((N ∈ NC ∧ M ∈ NC ) →
(((N ↑_{c}
0_{c}) ≠ ∅ ∧ (M
↑_{c} 0_{c}) ≠ ∅) ↔ (N
↑_{c} M) ≠ ∅)) 

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

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

⊢ (M ∈ NC →
((M ↑_{c}
0_{c}) ≠ ∅ ↔
(M ↑_{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.)

⊢ ((M ∈ NC ∧ (M
↑_{c} 0_{c}) ∈ NC ) → ∃a M = Nc ℘_{1}a) 

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

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

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

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

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

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

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

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

⊢ (A ∈ 2_{c} ↔ ∃x∃y(x ≠ y ∧ A = {x, y})) 

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

⊢ A ∈ V ⇒ ⊢ (M = Nc ℘_{1}A → (2_{c}
↑_{c} M) = Nc ℘A) 

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 V 

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.)

⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A ⊆ B →
Nc A
≤_{c} Nc B) 

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.)

⊢ ((A ∈ V ∧ A ≠ ∅) → A
≤_{c} A) 

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.)

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

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.)

⊢ ((A ∈ V ∧ A ≠ ∅) → 0_{c} ≤_{c}
A) 

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

⊢ ((A ∈ V ∧ A ≠ ∅) → A
≤_{c} Nc V) 

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.)

⊢ (A ∈ NC →
0_{c} ≤_{c} A) 