Home New Foundations ExplorerTheorem List (p. 62 of 64) < Previous  Next > Browser slow? Try the Unicode 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

Definitiondf-muc 6102* Define cardinal multiplication. Definition from [Rosser] p. 378. (Contributed by Scott Fenton, 24-Feb-2015.)
·c NC NC

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 NC Nc 1

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

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

Definitiondf-ce 6106* Define cardinal exponentiation. Definition from [Rosser] p. 381. (Contributed by Scott Fenton, 24-Feb-2015.)
c NC NC 1 1

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

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

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

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

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

Theorembrlecg 6112* Binary relationship form of cardinal less than or equal. (Contributed by SF, 24-Feb-2015.)
c

Theorembrlec 6113* Binary relationship form of cardinal less than or equal. (Contributed by SF, 24-Feb-2015.)
c

Theorembrltc 6114 Binary relationship form of cardinal less than. (Contributed by SF, 4-Mar-2015.)
c c

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

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

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

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

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

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

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

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

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

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

Theoremeqncg 6126 Equality of cardinalities. (Contributed by SF, 24-Feb-2015.)
Nc Nc

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

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

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

Theoremovmuc 6130* The value of cardinal multiplication. (Contributed by SF, 10-Mar-2015.)
NC NC ·c

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

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

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

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

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

Theoremncdisjun 6136 Cardinality of disjoint union of two sets. (Contributed by SF, 24-Feb-2015.)
Nc Nc Nc

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.)
1c Nc

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

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

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

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

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

Theoremnnnc 6146 A finite cardinal number is a cardinal number. (Contributed by SF, 24-Feb-2015.)
Nn 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.)
NC NC

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

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

Theoremncssfin 6151 A cardinal is finite iff it is a subset of Fin. (Contributed by SF, 25-Feb-2015.)
NC Nn 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.)
Nc Nc Nc 1 Nc 1

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

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 1c 2c

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

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

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

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.)
NC NC Nc 1

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

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

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.)
NC 1 Tc

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

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

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

Theoremovcelem1 6171* Lemma for ovce 6172. Set up stratification for the result. (Contributed by SF, 6-Mar-2015.)
1 1

Theoremovce 6172* The value of cardinal exponentiation. (Contributed by SF, 3-Mar-2015.)
NC NC c 1 1

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

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

Theoremelce 6175* Membership in cardinal exponentiation. Theorem XI.2.38 of [Rosser] p. 382. (Contributed by SF, 6-Mar-2015.)
NC NC c 1 1

Theoremfnce 6176 Functionhood statement for cardinal exponentiation. (Contributed by SF, 6-Mar-2015.)
c 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.)
NC c 0c 1

Theoremce0nnuli 6178 Inference form of ce0nnul 6177. (Contributed by SF, 9-Mar-2015.)
NC 1 c 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.)
NC NC c 0c c 0c c 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.)
Nn c 0c

Theoremcenc 6181 Cardinal exponentiation in terms of cardinality. Theorem XI.2.39 of [Rosser] p. 382. (Contributed by SF, 6-Mar-2015.)
Nc 1 c Nc 1 Nc

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.)
NC NC c 0c c 0c c

Theoremceclb 6183 Biconditional closure law for cardinal exponentiation. Theorem XI.2.48 of [Rosser] p. 384. (Contributed by SF, 9-Mar-2015.)
NC NC c 0c c 0c c 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.)
NC c 0c c 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.)
NC c 0c NC Nc 1

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

Theoremceclr 6187 Reverse closure law for cardinal exponentiation. (Contributed by SF, 13-Mar-2015.)
NC NC c NC c 0c NC c 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.)
Nn NC c 0c NC c NC

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

Theoremel2c 6191* Membership in cardinal two. (Contributed by SF, 3-Mar-2015.)
2c

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

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

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 1 1c Nc 1c

Theoremnclec 6195 A relationship between cardinality, subset, and cardinal less than. (Contributed by SF, 17-Mar-2015.)
Nc c Nc

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

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

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

Theoremlecncvg 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, 4-Mar-2015.)
c Nc

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.)
NC 0c c

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 >