HomeHome New Foundations Explorer
Theorem List (p. 63 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 - 6201-6300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremncpw1pwneg 6201 The cardinality of a unit power class is not equal to the cardinality of the power class. Theorem XI.2.4 of [Rosser] p. 372. (Contributed by SF, 10-Mar-2015.)
Nc 1 Nc
 
Theoremltcpw1pwg 6202 The cardinality of a unit power class is strictly less than the cardinality of the power class. Theorem XI.2.17 of [Rosser] p. 376. (Contributed by SF, 10-Mar-2015.)
Nc 1 <c Nc
 
Theoremsbthlem1 6203 Lemma for sbth 6206. Set up similarity with a range. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 11-Mar-2015.)
   &       &    Clos1    &       &       &       &       =>   
 
Theoremsbthlem2 6204 Lemma for sbth 6206. Eliminate hypotheses from sbthlem1 6203. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 10-Mar-2015.)
   =>   
 
Theoremsbthlem3 6205 Lemma for sbth 6206. If is equinumerous with a subset of and vice-versa, then is equinumerous with . Theorem XI.1.15 of [Rosser] p. 353. (Contributed by SF, 10-Mar-2015.)
 
Theoremsbth 6206 The Schroder-Bernstein Theorem. This theorem gives the antisymmetry law for cardinal less than or equal. Translated out, it means that, if is no larger than and is no larger than , then Nc Nc . Theorem XI.2.20 of [Rosser] p. 376. (Contributed by SF, 11-Mar-2015.)
NC NC <_c <_c
 
Theoremltlenlec 6207 Cardinal less than is equivalent to one-way cardinal less than or equal. Theorem XI.2.21 of [Rosser] p. 377. (Contributed by SF, 11-Mar-2015.)
NC NC <c <_c <_c
 
Theoremaddlec 6208 For nonempty sets, cardinal sum always increases cardinal less than or equal. Theorem XI.2.19 of [Rosser] p. 376. (Contributed by SF, 11-Mar-2015.)
<_c
 
Theoremaddlecncs 6209 For cardinals, cardinal sum always increases cardinal less than or equal. Corollary of theorem XI.2.19 of [Rosser] p. 376. (Contributed by SF, 11-Mar-2015.)
NC NC <_c
 
Theoremdflec2 6210* Cardinal less than or equal in terms of cardinal addition. Theorem XI.2.22 of [Rosser] p. 377. (Contributed by SF, 11-Mar-2015.)
NC NC <_c NC
 
Theoremlectr 6211 Cardinal less than or equal is transitive. (Contributed by SF, 12-Mar-2015.)
NC NC NC <_c <_c <_c
 
Theoremleltctr 6212 Transitivity law for cardinal less than or equal and less than. (Contributed by SF, 16-Mar-2015.)
NC NC NC <_c <c <c
 
Theoremlecponc 6213 Cardinal less than or equal partially orders the cardinals. (Contributed by SF, 12-Mar-2015.)
<_c Po NC
 
Theoremleaddc1 6214 Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
NC NC NC <_c <_c
 
Theoremleaddc2 6215 Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
NC NC NC <_c <_c
 
Theoremnc0le1 6216 Any cardinal is either zero or no greater than one. Theorem XI.2.24 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
NC 0c 1c <_c
 
Theoremnc0suc 6217* Any cardinal is either zero or the successor of a cardinal. Corollary of theorem XI.2.24 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
NC 0c NC 1c
 
Theoremleconnnc 6218 Cardinal less than or equal is total over the naturals. (Contributed by SF, 12-Mar-2015.)
Nn Nn <_c <_c
 
Theoremaddceq0 6219 The sum of two cardinals is zero iff both addends are zero. (Contributed by SF, 12-Mar-2015.)
NC NC 0c 0c 0c
 
Theoremce2lt 6220 Ordering law for cardinal exponentiation to two. Theorem XI.2.71 of [Rosser] p. 390. (Contributed by SF, 13-Mar-2015.)
NC c 0c NC <c 2cc
 
Theoremdflec3 6221* Another potential definition of cardinal inequality. (Contributed by SF, 23-Mar-2015.)
NC NC <_c
 
Theoremnclenc 6222* Comparison rule for cardinalities. (Contributed by SF, 24-Mar-2015.)
   &       =>    Nc <_c Nc
 
Theoremlenc 6223* Less than or equal condition for the cardinality of a number. (Contributed by SF, 18-Mar-2015.)
   =>    NC <_c Nc
 
Theoremtcncg 6224 Compute the T-raising of a cardinality. (Contributed by SF, 23-Apr-2021.)
Tc Nc Nc 1
 
Theoremtcnc 6225 Compute the T-raising of a cardinality. (Contributed by SF, 4-Mar-2015.)
   =>    Tc Nc Nc 1
 
Theoremtcncv 6226 Compute the T-raising of the cardinality of the universe. Part of Theorem 5.2 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
Tc Nc Nc 1c
 
Theoremtcnc1c 6227 Compute the T-raising of the cardinality of one. Part of Theorem 5.2 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
Tc Nc 1c Nc 1 1c
 
Theoremtc11 6228 Cardinal T is one-to-one. Based on theorem 2.4 of [Specker] p. 972. (Contributed by SF, 10-Mar-2015.)
NC NC Tc Tc
 
Theoremtaddc 6229* T raising rule for cardinal sum. (Contributed by SF, 11-Mar-2015.)
NC NC NC Tc Tc NC Tc
 
Theoremtlecg 6230 T-raising perserves order for cardinals. Theorem 5.5 of [Specker] p. 973. (Contributed by SF, 11-Mar-2015.)
NC NC <_c Tc <_c Tc
 
Theoremletc 6231* If a cardinal is less than or equal to a T-raising, then it is also a T-raising. Theorem 5.6 of [Specker] p. 973. (Contributed by SF, 11-Mar-2015.)
NC NC <_c Tc NC Tc
 
Theoremce0t 6232* If c 0c is a cardinal, then is a T-raising of some cardinal. (Contributed by SF, 17-Mar-2015.)
NC c 0c NC NC Tc
 
Theoremce2le 6233 Partial ordering law for base two cardinal exponentiation. Theorem 4.8 of [Specker] p. 973. (Contributed by SF, 16-Mar-2015.)
NC NC c 0c NC <_c 2cc <_c 2cc
 
Theoremcet 6234 The exponent of a T-raising to a T-raising is always a cardinal. (Contributed by SF, 13-Mar-2015.)
NC NC Tc c Tc NC
 
Theoremce2t 6235 The exponent of two to a T-raising is always a cardinal. Theorem 5.8 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
NC 2cc Tc NC
 
Theoremtce2 6236 Distributive law for T-raising and cardinal exponentiation to two. (Contributed by SF, 13-Mar-2015.)
NC c 0c NC Tc 2cc 2cc Tc
 
Theoremte0c 6237 A T-raising raised to zero is always a cardinal. (Contributed by SF, 16-Mar-2015.)
NC Tc c 0c NC
 
Theoremce0tb 6238* c 0c is a cardinal iff is a T-raising of some cardinal. (Contributed by SF, 17-Mar-2015.)
NC c 0c NC NC Tc
 
Theoremce0lenc1 6239 Cardinal exponentiation to zero is a cardinal iff the number is less than the size of cardinal one. (Contributed by SF, 18-Mar-2015.)
NC c 0c NC <_c Nc 1c
 
Theoremtlenc1c 6240 A T-raising is less than or equal to the cardinality of cardinal one. (Contributed by SF, 16-Mar-2015.)
NC Tc <_c Nc 1c
 
Theorem1ne0c 6241 Cardinal one is not zero. (Contributed by SF, 4-Mar-2015.)
1c 0c
 
Theorem2ne0c 6242 Cardinal two is not zero. (Contributed by SF, 4-Mar-2015.)
2c 0c
 
Theoremfinnc 6243 A set is finite iff its cardinality is a natural. (Contributed by SF, 18-Mar-2015.)
Fin Nc Nn
 
Theoremtcfnex 6244 The stratified T raising function is a set. (Contributed by SF, 18-Mar-2015.)
TcFn
 
Theoremfntcfn 6245 Functionhood statement for the stratified T-raising function. (Contributed by SF, 18-Mar-2015.)
TcFn 1c
 
Theorembrtcfn 6246 Binary relationship form of the stratified T-raising function. (Contributed by SF, 18-Mar-2015.)
   =>    TcFn Tc
 
Theoremncfin 6247 The cardinality of a set is a natural iff the set is finite. (Contributed by SF, 19-Mar-2015.)
   =>    Nc Nn Fin
 
Theoremnclennlem1 6248* Lemma for nclenn 6249. Set up stratification for induction. (Contributed by SF, 19-Mar-2015.)
NC <_c Nn
 
Theoremnclenn 6249 A cardinal that is less than or equal to a natural is a natural. Theorem XI.3.3 of [Rosser] p. 391. (Contributed by SF, 19-Mar-2015.)
NC Nn <_c Nn
 
Theoremaddcdi 6250 Distributivity law for cardinal addition and multiplication. Theorem XI.2.31 of [Rosser] p. 379. (Contributed by Scott Fenton, 31-Jul-2019.)
NC NC NC ·c ·c ·c
 
Theoremaddcdir 6251 Distributivity law for cardinal addition and multiplication. Theorem XI.2.30 of [Rosser] p. 379. (Contributed by Scott Fenton, 31-Jul-2019.)
NC NC NC ·c ·c ·c
 
Theoremmuc0or 6252 The cardinal product of two cardinal numbers is zero iff one of the numbers is zero. Biconditional form of theorem XI.2.34 of [Rosser] p. 380. (Contributed by Scott Fenton, 31-Jul-2019.)
NC NC ·c 0c 0c 0c
 
Theoremlemuc1 6253 Multiplication law for cardinal less than. Theorem XI.2.35 of [Rosser] p. 380. (Contributed by Scott Fenton, 31-Jul-2019.)
NC NC NC <_c ·c <_c ·c
 
Theoremlemuc2 6254 Multiplication law for cardinal less than. (Contributed by Scott Fenton, 31-Jul-2019.)
NC NC NC <_c ·c <_c ·c
 
Theoremncslemuc 6255 A cardinal is less than or equal to its product with another. Theorem XI.2.36 of [Rosser] p. 381. (Contributed by Scott Fenton, 31-Jul-2019.)
NC NC 0c <_c ·c
 
Theoremncvsq 6256 The product of the cardinality of squared is just the cardinality of . Theorem XI.2.37 of [Rosser] p. 381. (Contributed by Scott Fenton, 31-Jul-2019.)
Nc ·c Nc Nc
 
Theoremvvsqenvv 6257 There are exactly as many ordered pairs as there are sets. Corollary to theorem XI.2.37 of [Rosser] p. 381. (Contributed by Scott Fenton, 31-Jul-2019.)
 
Theorem0lt1c 6258 Cardinal one is strictly greater than cardinal zero. (Contributed by Scott Fenton, 1-Aug-2019.)
0c <c 1c
 
Theoremcsucex 6259 The function mapping to its cardinal successor exists. (Contributed by Scott Fenton, 30-Jul-2019.)
1c
 
Theorembrcsuc 6260* Binary relationship form of the successor mapping function. (Contributed by Scott Fenton, 2-Aug-2019.)
   &       =>    1c 1c
 
Theoremnnltp1clem1 6261 Lemma for nnltp1c 6262. Set up stratification. (Contributed by SF, 25-Mar-2015.)
<c 1c
 
Theoremnnltp1c 6262 Any natural is less than one plus itself. (Contributed by SF, 25-Mar-2015.)
Nn <c 1c
 
Theoremaddccan2nclem1 6263* Lemma for addccan2nc 6265. Stratification helper theorem. (Contributed by Scott Fenton, 2-Aug-2019.)
AddC
 
Theoremaddccan2nclem2 6264* Lemma for addccan2nc 6265. Establish stratification for induction. (Contributed by Scott Fenton, 2-Aug-2019.)
 
Theoremaddccan2nc 6265 Cancellation law for addition over the cardinal numbers. Biconditional form of theorem XI.3.2 of [Rosser] p. 391. (Contributed by Scott Fenton, 2-Aug-2019.)
Nn NC NC
 
Theoremlecadd2 6266 Cardinal addition preserves cardinal less than. Biconditional form of corollary 4 of theorem XI.3.2 of [Rosser] p. 391. (Contributed by Scott Fenton, 2-Aug-2019.)
Nn NC NC <_c <_c
 
Theoremncslesuc 6267 Relationship between successor and cardinal less than or equal. (Contributed by Scott Fenton, 3-Aug-2019.)
NC NC <_c 1c <_c 1c
 
Theoremnmembers1lem1 6268* Lemma for nmembers1 6271. Set up stratification. (Contributed by SF, 25-Mar-2015.)
Nn 1c <_c <_c Tc Tc
 
Theoremnmembers1lem2 6269 Lemma for nmembers1 6271. The set of all elements between one and zero is empty. (Contributed by Scott Fenton, 1-Aug-2019.)
Nn 1c <_c <_c 0c 0c
 
Theoremnmembers1lem3 6270* Lemma for nmembers1 6271. If the interval from one to a natural is in a given natural, extending it by one puts it in the next natural. (Contributed by Scott Fenton, 3-Aug-2019.)
Nn Nn Nn 1c <_c <_c Nn 1c <_c <_c 1c 1c
 
Theoremnmembers1 6271* Count the number of elements in a natural interval. From nmembers1lem2 6269 and nmembers1lem3 6270, we would expect to arrive at Nn 1c <_c <_c , but this proposition is not stratifiable. Instead, we arrive at the weaker conclusion below. We can arrive at the earlier proposition once we add the Axiom of Counting, which we will do later. (Contributed by Scott Fenton, 3-Aug-2019.)
Nn Nn 1c <_c <_c Tc Tc
 
Theoremltcirr 6272 Cardinal less than is irreflexive. (Contributed by Scott Fenton, 12-Dec-2021.)
<c
 
2.4.6  Specker's disproof of the axiom of choice
 
Syntaxcspac 6273 Extend the definition of a class to include the special set generator for the axiom of choice.
Spac
 
Definitiondf-spac 6274* Define the special class generator for the disproof of the axiom of choice. Definition 6.1 of [Specker] p. 973. (Contributed by SF, 3-Mar-2015.)
Spac NC Clos1 NC NC 2cc
 
Theoremnncdiv3lem1 6275 Lemma for nncdiv3 6277. Set up a helper for stratification. (Contributed by SF, 3-Mar-2015.)
Ins3 AddC AddC
 
Theoremnncdiv3lem2 6276* Lemma for nncdiv3 6277. Set up stratification for induction. (Contributed by SF, 2-Mar-2015.)
Nn 1c 2c
 
Theoremnncdiv3 6277* Divisibility by three rule for finite cardinals. Part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 2-Mar-2015.)
Nn Nn 1c 2c
 
Theoremnnc3n3p1 6278 Three times a natural is not one more than three times a natural. Another part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
Nn Nn 1c
 
Theoremnnc3n3p2 6279 Three times a natural is not two more than three times a natural. Another part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 12-Mar-2015.)
Nn Nn 2c
 
Theoremnnc3p1n3p2 6280 One more than three times a natural is not two more than three times a natural. Final part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 12-Mar-2015.)
Nn Nn 1c 2c
 
Theoremspacvallem1 6281* Lemma for spacval 6282. Set up stratification for the recursive relationship. (Contributed by SF, 6-Mar-2015.)
NC NC 2cc
 
Theoremspacval 6282* The value of the special set generator. (Contributed by SF, 4-Mar-2015.)
NC Spac Clos1 NC NC 2cc
 
Theoremfnspac 6283 The special set generator is a function over the cardinals. (Contributed by SF, 18-Mar-2015.)
Spac NC
 
Theoremspacssnc 6284 The special set generator generates a set of cardinals. (Contributed by SF, 13-Mar-2015.)
NC Spac NC
 
Theoremspacid 6285 The initial value of the special set generator is an element. (Contributed by SF, 13-Mar-2015.)
NC Spac
 
Theoremspaccl 6286 Closure law for the special set generator. (Contributed by SF, 13-Mar-2015.)
NC Spac c 0c NC 2cc Spac
 
Theoremspacind 6287* Inductive law for the special set generator. (Contributed by SF, 13-Mar-2015.)
NC Spac c 0c NC 2cc Spac
 
Theoremspacis 6288* Induction scheme for the special set generator. (Contributed by SF, 13-Mar-2015.)
   &       &       &    2cc    &       &    NC    &    NC Spac c 0c NC    =>    NC Spac
 
Theoremnchoicelem1 6289 Lemma for nchoice 6308. A finite cardinal is not one more than its T-raising. (Contributed by SF, 3-Mar-2015.)
Nn Tc 1c
 
Theoremnchoicelem2 6290 Lemma for nchoice 6308. A finite cardinal is not two more than its T-raising. (Contributed by SF, 12-Mar-2015.)
Nn Tc 2c
 
Theoremnchoicelem3 6291 Lemma for nchoice 6308. Compute the value of Spac when the argument is not exponentiable. Theorem 6.2 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
NC c 0c NC Spac
 
Theoremnchoicelem4 6292 Lemma for nchoice 6308. The initial value of Spac is a minimum value. Theorem 6.4 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
NC Spac <_c
 
Theoremnchoicelem5 6293 Lemma for nchoice 6308. A cardinal is not a member of the special set of itself raised to two. Theorem 6.5 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
NC c 0c NC Spac 2cc
 
Theoremnchoicelem6 6294 Lemma for nchoice 6308. Split the special set generator into base and inductive values. Theorem 6.6 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
NC c 0c NC Spac Spac 2cc
 
Theoremnchoicelem7 6295 Lemma for nchoice 6308. Calculate the cardinality of a special set generator. Theorem 6.7 of [Specker] p. 974. (Contributed by SF, 13-Mar-2015.)
NC c 0c NC Nc Spac Nc Spac 2cc 1c
 
Theoremnchoicelem8 6296 Lemma for nchoice 6308. An anti-closure condition for cardinal exponentiation to zero. Theorem 4.5 of [Specker] p. 973. (Contributed by SF, 18-Mar-2015.)
<_c We NC NC c 0c NC Nc 1c <c
 
Theoremnchoicelem9 6297 Lemma for nchoice 6308. Calculate the cardinality of the special set generator when near the end of raisability. Theorem 6.8 of [Specker] p. 974. (Contributed by SF, 18-Mar-2015.)
<_c We NC NC c 0c NC Nc Spac Tc 2c Nc Spac Tc 3c
 
Theoremnchoicelem10 6298 Lemma for nchoice 6308. Stratification helper lemma. (Contributed by SF, 18-Mar-2015.)
   &       =>    Ins3 S Ins2 S S S Image1c Clos1
 
Theoremnchoicelem11 6299* Lemma for nchoice 6308. Set up stratification for nchoicelem12 6300. (Contributed by SF, 18-Mar-2015.)
NC Nc Spac Tc Nc Spac Nn
 
Theoremnchoicelem12 6300 Lemma for nchoice 6308. If the T-raising of a cardinal yields a finite special set, then so does the initial set. Theorem 7.1 of [Specker] p. 974. (Contributed by SF, 18-Mar-2015.)
NC Spac Tc Fin Spac Fin
    < 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 >