 Home New Foundations ExplorerTheorem List (p. 62 of 64) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 6101-6200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Definitiondf-nc 6101 Define the cardinality operation. This is the unique cardinal number containing a given set. Definition from [Rosser] p. 371. (Contributed by Scott Fenton, 24-Feb-2015.)
Nc A = [A] ≈

Definitiondf-muc 6102* Define cardinal multiplication. Definition from [Rosser] p. 378. (Contributed by Scott Fenton, 24-Feb-2015.)
·c = (m NC , n NC {a b m g n a ≈ (b × g)})

Definitiondf-tc 6103* Define the type-raising 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, 24-Feb-2015.)
Tc A = (℩b(b NC x A b = Nc 1x))

Definitiondf-2c 6104 Define cardinal two. This is the set of all sets with two unique elements. (Contributed by Scott Fenton, 24-Feb-2015.)
2c = Nc {, V}

Definitiondf-3c 6105 Define cardinal three. This is the set of all sets with three unique elements. (Contributed by Scott Fenton, 24-Feb-2015.)
3c = Nc {, V, (V {})}

Definitiondf-ce 6106* Define cardinal exponentiation. Definition from [Rosser] p. 381. (Contributed by Scott Fenton, 24-Feb-2015.)
c = (n NC , m NC {g ab(1a n 1b m g ≈ (am b))})

Definitiondf-tcfn 6107 Define the stratified T-raising function. (Contributed by Scott Fenton, 24-Feb-2015.)
TcFn = (x 1c Tc x)

Theoremnceq 6108 Cardinality equality law. (Contributed by SF, 24-Feb-2015.)
(A = BNc A = Nc B)

Theoremnceqi 6109 Equality inference for cardinality. (Contributed by SF, 24-Feb-2015.)
A = B        Nc A = Nc B

Theoremnceqd 6110 Equality deduction for cardinality. (Contributed by SF, 24-Feb-2015.)
(φA = B)       (φNc A = Nc B)

Theoremncsex 6111 The class of all cardinal numbers is a set. (Contributed by SF, 24-Feb-2015.)
NC V

Theorembrlecg 6112* Binary relationship form of cardinal less than or equal. (Contributed by SF, 24-Feb-2015.)
((A V B W) → (Ac Bx A y B x y))

Theorembrlec 6113* Binary relationship form of cardinal less than or equal. (Contributed by SF, 24-Feb-2015.)
A V    &   B V       (Ac Bx A y B x y)

Theorembrltc 6114 Binary relationship form of cardinal less than. (Contributed by SF, 4-Mar-2015.)
(A <c B ↔ (Ac B AB))

Theoremlecex 6115 Cardinal less than or equal is a set. (Contributed by SF, 24-Feb-2015.)
c V

Theoremltcex 6116 Cardinal strict less than is a set. (Contributed by SF, 24-Feb-2015.)
<c V

Theoremncex 6117 The cardinality of a class is a set. (Contributed by SF, 24-Feb-2015.)
Nc A V

Theoremnulnnc 6118 The empty class is not a cardinal number. (Contributed by SF, 24-Feb-2015.)
¬ NC

Theoremelncs 6119* Membership in the cardinals. (Contributed by SF, 24-Feb-2015.)
(A NCx A = Nc x)

Theoremncelncs 6120 The cardinality of a set is a cardinal number. (Contributed by SF, 24-Feb-2015.)
(A VNc A NC )

Theoremncelncsi 6121 The cardinality of a set is a cardinal number. (Contributed by SF, 10-Mar-2015.)
A V        Nc A NC

Theoremncidg 6122 A set is a member of its own cardinal. (Contributed by SF, 24-Feb-2015.)
(A VA Nc A)

Theoremncid 6123 A set is a member of its own cardinal. (Contributed by SF, 24-Feb-2015.)
A V       A Nc A

Theoremncprc 6124 The cardinality of a proper class is the empty set. (Contributed by SF, 24-Feb-2015.)
A V → Nc A = )

Theoremelnc 6125 Membership in cardinality. (Contributed by SF, 24-Feb-2015.)
(A Nc BAB)

Theoremeqncg 6126 Equality of cardinalities. (Contributed by SF, 24-Feb-2015.)
(A V → ( Nc A = Nc BAB))

Theoremeqnc 6127 Equality of cardinalities. (Contributed by SF, 24-Feb-2015.)
A V       ( Nc A = Nc BAB)

Theoremncseqnc 6128 A cardinal is equal to the cardinality of a set iff it contains the set. (Contributed by SF, 24-Feb-2015.)
(A NC → (A = Nc XX A))

Theoremeqnc2 6129 Alternate condition for equality to a cardinality. (Contributed by SF, 18-Mar-2015.)
X V       (A = Nc X ↔ (A NC X A))

Theoremovmuc 6130* The value of cardinal multiplication. (Contributed by SF, 10-Mar-2015.)
((M NC N NC ) → (M ·c N) = {a b M g N a ≈ (b × g)})

Theoremmucnc 6131 Cardinal multiplication in terms of cardinality. Theorem XI.2.27 of [Rosser] p. 378. (Contributed by SF, 10-Mar-2015.)
A V    &   B V       ( Nc A ·c Nc B) = Nc (A × B)

Theoremmuccl 6132 Closure law for cardinal multiplicaton. (Contributed by SF, 10-Mar-2015.)
((A NC B NC ) → (A ·c B) NC )

Theoremmucex 6133 Cardinal multiplication is a set. (Contributed by SF, 24-Feb-2015.)
·c V

Theoremmuccom 6134 Cardinal multiplication commutes. Theorem XI.2.28 of [Rosser] p. 378. (Contributed by SF, 10-Mar-2015.)
((A NC B NC ) → (A ·c B) = (B ·c A))

Theoremmucass 6135 Cardinal multiplication associates. Theorem XI.2.29 of [Rosser] p. 378. (Contributed by SF, 10-Mar-2015.)
((A NC B NC C NC ) → ((A ·c B) ·c C) = (A ·c (B ·c C)))

Theoremncdisjun 6136 Cardinality of disjoint union of two sets. (Contributed by SF, 24-Feb-2015.)
A V    &   B V       ((AB) = Nc (AB) = ( Nc A +c Nc B))

Theoremdf0c2 6137 Cardinal zero is the cardinality of the empty set. Theorem XI.2.7 of [Rosser] p. 372. (Contributed by SF, 24-Feb-2015.)
0c = Nc

Theorem0cnc 6138 Cardinal zero is a cardinal number. Corollary 1 to theorem XI.2.7 of [Rosser] p. 373. (Contributed by SF, 24-Feb-2015.)
0c NC

Theorem1cnc 6139 Cardinal one is a cardinal number. Corollary 2 to theorem XI.2.8 of [Rosser] p. 373. (Contributed by SF, 24-Feb-2015.)
1c NC

Theoremdf1c3 6140 Cardinal one is the cardinality of a singleton. Theorem XI.2.8 of [Rosser] p. 373. (Contributed by SF, 2-Mar-2015.)
A V       1c = Nc {A}

Theoremdf1c3g 6141 Cardinal one is the cardinality of a singleton. Theorem XI.2.8 of [Rosser] p. 373. (Contributed by SF, 13-Mar-2015.)
(A V → 1c = Nc {A})

Theoremmuc0 6142 Cardinal multiplication by zero. Theorem XI.2.32 of [Rosser] p. 379. (Contributed by SF, 10-Mar-2015.)
(A NC → (A ·c 0c) = 0c)

Theoremmucid1 6143 Cardinal multiplication by one. (Contributed by SF, 11-Mar-2015.)
(A NC → (A ·c 1c) = A)

Theoremncaddccl 6144 The cardinals are closed under cardinal addition. Theorem XI.2.10 of [Rosser] p. 374. (Contributed by SF, 24-Feb-2015.)
((A NC B NC ) → (A +c B) NC )

Theorempeano2nc 6145 The successor of a cardinal is a cardinal. (Contributed by SF, 24-Feb-2015.)
(A NC → (A +c 1c) NC )

Theoremnnnc 6146 A finite cardinal number is a cardinal number. (Contributed by SF, 24-Feb-2015.)
(A NnA NC )

Theoremnnssnc 6147 The finite cardinals are a subset of the cardinals. Theorem XI.2.11 of [Rosser] p. 374. (Contributed by SF, 24-Feb-2015.)
Nn NC

Theoremncdisjeq 6148 Two cardinals are either disjoint or equal. (Contributed by SF, 25-Feb-2015.)
((A NC B NC ) → ((AB) = A = B))

Theoremnceleq 6149 If two cardinals have an element in common, then they are equal. (Contributed by SF, 25-Feb-2015.)
(((A NC B NC ) (X A X B)) → A = B)

Theorempeano4nc 6150 Successor is one-to-one over the cardinals. Theorem XI.2.12 of [Rosser] p. 375. (Contributed by SF, 25-Feb-2015.)
((A NC B NC ) → ((A +c 1c) = (B +c 1c) ↔ A = B))

Theoremncssfin 6151 A cardinal is finite iff it is a subset of Fin. (Contributed by SF, 25-Feb-2015.)
(A NC → (A NnA Fin ))

Theoremncpw1 6152 The cardinality of two sets are equal iff their unit power classes have the same cardinality. (Contributed by SF, 25-Feb-2015.)
A V       ( Nc A = Nc BNc 1A = Nc 1B)

Theoremncpwpw1 6153 Power class and unit power class commute within cardinality. (Contributed by SF, 26-Feb-2015.)
A V        Nc 1A = Nc 1A

Theoremncpw1c 6154 The cardinality of 1c is equal to that of its power class. (Contributed by SF, 26-Feb-2015.)
Nc 1c = Nc 1c

Theorem1p1e2c 6155 One plus one equals two. Theorem *110.64 of [WhiteheadRussell] p. 86. This theorem is occasionally useful. (Contributed by SF, 2-Mar-2015.)
(1c +c 1c) = 2c

Theorem2p1e3c 6156 Two plus one equals three. (Contributed by SF, 2-Mar-2015.)
(2c +c 1c) = 3c

Theoremtcex 6157 The cardinal T operation always yields a set. (Contributed by SF, 2-Mar-2015.)
Tc A V

Theoremtceq 6158 Equality theorem for cardinal T operator. (Contributed by SF, 2-Mar-2015.)
(A = BTc A = Tc B)

Theoremncspw1eu 6159* Given a cardinal, there is a unique cardinal that contains the unit power class of its members. (Contributed by SF, 2-Mar-2015.)
(A NC∃!x NC y A x = Nc 1y)

Theoremtccl 6160 The cardinal T operation over a cardinal yields a cardinal. (Contributed by SF, 2-Mar-2015.)
(A NCTc A NC )

Theoremeqtc 6161* The defining property of the cardinal T operation. (Contributed by SF, 2-Mar-2015.)
(A NC → ( Tc A = Bx A B = Nc 1x))

Theorempw1eltc 6162 The unit power class of an element of a cardinal is in the cardinal's T raising. (Contributed by SF, 2-Mar-2015.)
((A NC B A) → 1B Tc A)

Theoremtc0c 6163 The T raising of cardinal zero is still cardinal zero. (Contributed by SF, 2-Mar-2015.)
Tc 0c = 0c

Theoremtcdi 6164 T raising distributes over addition. (Contributed by SF, 2-Mar-2015.)
((A NC B NC ) → Tc (A +c B) = ( Tc A +c Tc B))

Theoremtc1c 6165 T raising does not change cardinal one. (Contributed by SF, 2-Mar-2015.)
Tc 1c = 1c

Theoremtc2c 6166 T raising does not change cardinal two. (Contributed by SF, 2-Mar-2015.)
Tc 2c = 2c

Theorem2nnc 6167 Two is a finite cardinal. (Contributed by SF, 4-Mar-2015.)
2c Nn

Theorem2nc 6168 Two is a cardinal number. (Contributed by SF, 3-Mar-2015.)
2c NC

Theorempw1fin 6169 The unit power class of a finite set is finite. (Contributed by SF, 3-Mar-2015.)
(A Fin1A Fin )

Theoremnntccl 6170 Cardinal T is closed under the natural numbers. (Contributed by SF, 3-Mar-2015.)
(A NnTc A Nn )

Theoremovcelem1 6171* Lemma for ovce 6172. Set up stratification for the result. (Contributed by SF, 6-Mar-2015.)
((N V M W) → {g ab(1a N 1b M g ≈ (am b))} V)

Theoremovce 6172* The value of cardinal exponentiation. (Contributed by SF, 3-Mar-2015.)
((N NC M NC ) → (Nc M) = {g ab(1a N 1b M g ≈ (am b))})

Theoremceexlem1 6173* Lemma for ceex 6174. Set up part of the stratification. (Contributed by SF, 6-Mar-2015.)
({{a}}, n ( S SI Pw1Fn ) ↔ 1a n)

Theoremceex 6174 Cardinal exponentiation is stratified. (Contributed by SF, 3-Mar-2015.)
c V

Theoremelce 6175* Membership in cardinal exponentiation. Theorem XI.2.38 of [Rosser] p. 382. (Contributed by SF, 6-Mar-2015.)
((N NC M NC ) → (A (Nc M) ↔ xy(1x N 1y M A ≈ (xm y))))

Theoremfnce 6176 Functionhood statement for cardinal exponentiation. (Contributed by SF, 6-Mar-2015.)
c Fn ( NC × NC )

Theoremce0nnul 6177* A condition for cardinal exponentiation being non-empty. Theorem XI.2.42 of [Rosser] p. 382. (Contributed by SF, 6-Mar-2015.)
(M NC → ((Mc 0c) ≠ a1a M))

Theoremce0nnuli 6178 Inference form of ce0nnul 6177. (Contributed by SF, 9-Mar-2015.)
((M NC 1A M) → (Mc 0c) ≠ )

Theoremce0addcnnul 6179 The sum of two cardinals raised to 0c is non-empty iff each addend raised to 0c is non-empty. Theorem XI.2.43 of [Rosser] p. 383. (Contributed by SF, 9-Mar-2015.)
((M NC N NC ) → (((M +c N) ↑c 0c) ≠ ↔ ((Mc 0c) ≠ (Nc 0c) ≠ )))

Theoremce0nn 6180 A natural raised to cardinal zero is non-empty. Theorem XI.2.44 of [Rosser] p. 383. (Contributed by SF, 9-Mar-2015.)
(N Nn → (Nc 0c) ≠ )

Theoremcenc 6181 Cardinal exponentiation in terms of cardinality. Theorem XI.2.39 of [Rosser] p. 382. (Contributed by SF, 6-Mar-2015.)
A V    &   B V       ( Nc 1Ac Nc 1B) = Nc (Am B)

Theoremce0nnulb 6182 Cardinal exponentiation is non-empty iff the two sets raised to zero are non-empty. Theorem XI.2.47 of [Rosser] p. 384. (Contributed by SF, 9-Mar-2015.)
((N NC M NC ) → (((Nc 0c) ≠ (Mc 0c) ≠ ) ↔ (Nc M) ≠ ))

Theoremceclb 6183 Biconditional closure law for cardinal exponentiation. Theorem XI.2.48 of [Rosser] p. 384. (Contributed by SF, 9-Mar-2015.)
((M NC N NC ) → (((Mc 0c) ≠ (Nc 0c) ≠ ) ↔ (Mc N) NC ))

Theoremce0nulnc 6184 Cardinal exponentiation to zero is a cardinal iff it is non-empty. Corollary 1 of theorem XI.2.38 of [Rosser] p. 384. (Contributed by SF, 13-Mar-2015.)
(M NC → ((Mc 0c) ≠ ↔ (Mc 0c) NC ))

Theoremce0ncpw1 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, 9-Mar-2015.)
((M NC (Mc 0c) NC ) → a M = Nc 1a)

Theoremcecl 6186 Closure law for cardinal exponentiation. Corollary 3 of theorem XI.2.48 of [Rosser] p. 384. (Contributed by SF, 9-Mar-2015.)
(((M NC N NC ) ((Mc 0c) NC (Nc 0c) NC )) → (Mc N) NC )

Theoremceclr 6187 Reverse closure law for cardinal exponentiation. (Contributed by SF, 13-Mar-2015.)
((M NC N NC (Mc N) NC ) → ((Mc 0c) NC (Nc 0c) NC ))

Theoremfce 6188 Full functionhood statement for cardinal exponentiation. (Contributed by SF, 13-Mar-2015.)
c :( NC × NC )–→( NC ∪ {})

Theoremceclnn1 6189 Closure law for cardinal exponentiation when the base is a natural. (Contributed by SF, 13-Mar-2015.)
((M Nn N NC (Nc 0c) NC ) → (Mc N) NC )

Theoremce0 6190 The value of non-empty cardinal exponentiation. Theorem XI.2.49 of [Rosser] p. 385. (Contributed by SF, 9-Mar-2015.)
((M NC (Mc 0c) NC ) → (Mc 0c) = 1c)

Theoremel2c 6191* Membership in cardinal two. (Contributed by SF, 3-Mar-2015.)
(A 2cxy(xy A = {x, y}))

Theoremce2 6192 The value of base two cardinal exponentiation. Theorem XI.2.70 of [Rosser] p. 389. (Contributed by SF, 3-Mar-2015.)
A V       (M = Nc 1A → (2cc M) = Nc A)

Theoremce2nc1 6193 Compute an exponent of the cardinality of one. Theorem 4.3 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
(2cc Nc 1c) = Nc V

Theoremce2ncpw11c 6194 Compute an exponent of the cardinality of the unit power class of one. Theorem 4.4 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
(2cc Nc 11c) = Nc 1c

Theoremnclec 6195 A relationship between cardinality, subset, and cardinal less than. (Contributed by SF, 17-Mar-2015.)
A V    &   B V       (A BNc Ac Nc B)

Theoremlecidg 6196 A non-empty set is less than or equal to itself. Theorem XI.2.14 of [Rosser] p. 375. (Contributed by SF, 4-Mar-2015.)
((A V A) → Ac A)

Theoremnclecid 6197 A cardinal is less than or equal to itself. Corollary 1 of theorem XI.2.14 of [Rosser] p. 376. (Contributed by SF, 4-Mar-2015.)
(A NCAc A)

Theoremlec0cg 6198 Cardinal zero is a minimal element of cardinal less than or equal. Theorem XI.2.15 of [Rosser] p. 376. (Contributed by SF, 4-Mar-2015.)
((A V A) → 0cc A)

Theoremlecncvg 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, 4-Mar-2015.)
((A V A) → Ac Nc V)

Theoremle0nc 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, 12-Mar-2015.)
(A NC → 0cc A)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6337
 Copyright terms: Public domain < Previous  Next >