HomeHome New Foundations Explorer
Theorem 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 multiplication. (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 nonempty. 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 nonempty iff each addend raised to 0c is nonempty. 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 nonempty. 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 nonempty iff the two sets raised to zero are nonempty. 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 nonempty. 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 nonempty 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 nonempty 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
    < Previous  Next >

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-6338
  Copyright terms: Public domain < Previous  Next >