List of theorems referencing the symbol CARD

(190) Theorem 151: [Cardinality theorem] Card(#S) & Ord(#S) & (EXISTS f in OM | one_1_map(f) & (range(f) = S) & (domain(f) = #S))
(198) Theorem 159: [A cardinal is its own cardinality] Card(S) •eq (S = #S)
(199) Theorem 160: [Uniqueness of Cardinality] (Card(C) & (EXISTS f in OM | (one_1_map(f) & (range(f) = S) & domain(f) = C))) •imp (C = #S)
(223) Theorem 183: [0 is a finite cardinal] Ord(0) & Finite(0) & Card(0)
(241) Theorem 200: [All finite ordinals are cardinals] (Ord(X) & Finite(X)) •imp Card(X)
(247) Theorem 201: [The set of integers is an infinite ordinal consisting of all finite ordinals] Ord(Za) & (not Finite(Za)) & ((Card(X) & Finite(X)) •eq (X in Za))
(248) Theorem 202: [All integers are finite ordinals and cardinals] (X in Za) •imp ((X = #X) & Card(X) & Ord(X) & Finite(X))
(250) Theorem 204: [The set of integers is a Cardinal] Card(Za)
(251) Theorem 205: [The successor of an integer is an integer] (I in Za) •imp (Card(next(I)) & (next(I) in Za))
(252) Theorem 206: [The first few integers are all cardinals] Ord(0) & (0 in Za) & (1 in Za) & (2 in Za) & (3 in Za) & Card(0) & Card(1) & Card(2) & Card(3)
(325) Theorem 278: [Monotonicity of addition, 2] Card(M) •imp ((M •incin (I •PLUS M)) & (M •incin (M •PLUS I)))
(437) Theorem 344: (Card(O1) & Card(O2) & (not Finite(O1 + O2))) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f) | (EXISTS y in (O1 + O2) | range(f •ON x) •incin (y •PROD y))))