HomeHome New Foundations Explorer
Theorem List (p. 46 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 - 4501-4600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremtfinltfin 4501 Ordering rule for the finite T operation. Corollary to theorem X.1.33 of [Rosser] p. 529. (Contributed by SF, 1-Feb-2015.)
Nn Nn <fin Tfin Tfin <fin
 
Theoremtfinlefin 4502 Ordering rule for the finite T operation. Theorem X.1.33 of [Rosser] p. 529. (Contributed by SF, 2-Feb-2015.)
Nn Nn <_fin Tfin Tfin <_fin
 
Theoremevenfinex 4503 The set of all even naturals exists. (Contributed by SF, 20-Jan-2015.)
Evenfin
 
Theoremoddfinex 4504 The set of all odd naturals exists. (Contributed by SF, 20-Jan-2015.)
Oddfin
 
Theorem0ceven 4505 Cardinal zero is even. (Contributed by SF, 20-Jan-2015.)
0c Evenfin
 
Theoremevennn 4506 An even finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
Evenfin Nn
 
Theoremoddnn 4507 An odd finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
Oddfin Nn
 
Theoremevennnul 4508 An even number is nonempty. (Contributed by SF, 22-Jan-2015.)
Evenfin
 
Theoremoddnnul 4509 An odd number is nonempty. (Contributed by SF, 22-Jan-2015.)
Oddfin
 
Theoremsucevenodd 4510 The successor of an even natural is odd. (Contributed by SF, 20-Jan-2015.)
Evenfin 1c 1c Oddfin
 
Theoremsucoddeven 4511 The successor of an odd natural is even. (Contributed by SF, 22-Jan-2015.)
Oddfin 1c 1c Evenfin
 
Theoremdfevenfin2 4512* Alternate definition of even number. (Contributed by SF, 25-Jan-2015.)
Evenfin Nn
 
Theoremdfoddfin2 4513* Alternate definition of odd number. (Contributed by SF, 25-Jan-2015.)
Oddfin Nn 1c 1c
 
Theoremevenoddnnnul 4514 Every nonempty finite cardinal is either even or odd. Theorem X.1.35 of [Rosser] p. 529. (Contributed by SF, 20-Jan-2015.)
Evenfin Oddfin Nn
 
Theoremevenodddisjlem1 4515* Lemma for evenodddisj 4516. Establish stratification for induction. (Contributed by SF, 25-Jan-2015.)
Nn 1c 1c
 
Theoremevenodddisj 4516 The even finite cardinals and the odd ones are disjoint. Theorem X.1.36 of [Rosser] p. 529. (Contributed by SF, 22-Jan-2015.)
Evenfin Oddfin
 
Theoremeventfin 4517 If is even , then so is Tfin . Theorem X.1.37 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)
Evenfin Tfin Evenfin
 
Theoremoddtfin 4518 If is odd , then so is Tfin . Theorem X.1.38 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)
Oddfin Tfin Oddfin
 
Theoremnnadjoinlem1 4519* Lemma for nnadjoin 4520. Establish stratification. (Contributed by SF, 29-Jan-2015.)
 
Theoremnnadjoin 4520* Adjoining a new element to every member of does not change its size. Theorem X.1.39 of [Rosser] p. 530. (Contributed by SF, 29-Jan-2015.)
Nn
 
Theoremnnadjoinpw 4521 Adjoining an element to a power class. Theorem X.1.40 of [Rosser] p. 530. (Contributed by SF, 27-Jan-2015.)
Nn Nn
 
Theoremnnpweqlem1 4522* Lemma for nnpweq 4523. Establish stratification for induction. (Contributed by SF, 26-Jan-2015.)
Nn
 
Theoremnnpweq 4523* If two sets are the same finite size, then so are their power classes. Theorem X.1.41 of [Rosser] p. 530. (Contributed by SF, 26-Jan-2015.)
Nn Nn
 
Theoremsrelk 4524 Binary relationship form of the Sfin relationship. (Contributed by SF, 23-Jan-2015.)
   &       =>    Nn k Nn Ins3k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk Ins3k Sk Ins2k SIk Sk k1 1 1c Ins2k Sk k1 1 1ck1 1 1 1c Sfin
 
Theoremsrelkex 4525 The expression at the core of srelk 4524 exists. (Contributed by SF, 30-Jan-2015.)
Nn k Nn Ins3k Ins3k SIk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins2k Sk k1 1 1c Ins2k Ins3k SIk Ins3k Sk Ins2k SIk Sk k1 1 1c Ins2k Sk k1 1 1ck1 1 1 1c
 
Theoremsfineq1 4526 Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
Sfin Sfin
 
Theoremsfineq2 4527 Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
Sfin Sfin
 
Theoremsfin01 4528 Zero and one satisfy Sfin. Theorem X.1.42 of [Rosser] p. 530. (Contributed by SF, 30-Jan-2015.)
Sfin 0c 1c
 
Theoremsfin112 4529 Equality law for the finite S operator. Theorem X.1.43 of [Rosser] p. 530. (Contributed by SF, 27-Jan-2015.)
Sfin Sfin
 
Theoremsfindbl 4530* If the unit power set of a set is in the successor of a finite cardinal, then there is a natural that is smaller than the finite cardinal and whose double is smaller than the successor of the cardinal. Theorem X.1.44 of [Rosser] p. 531. (Contributed by SF, 30-Jan-2015.)
Nn 1 1c Nn Sfin Sfin 1c
 
Theoremsfintfinlem1 4531* Lemma for sfintfin 4532. Set up induction stratification. (Contributed by SF, 31-Jan-2015.)
Sfin Sfin Tfin Tfin
 
Theoremsfintfin 4532 If two numbers obey Sfin, then do their T raisings. Theorem X.1.45 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
Sfin Sfin Tfin Tfin
 
Theoremtfinnnlem1 4533* Lemma for tfinnn 4534. Establish stratification. (Contributed by SF, 30-Jan-2015.)
Nn Tfin Tfin
 
Theoremtfinnn 4534* T-raising of a set of naturals. Theorem X.1.46 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
Nn Nn Tfin Tfin
 
Theoremsfinltfin 4535 Ordering law for finite smaller than. Theorem X.1.47 of [Rosser] p. 532. (Contributed by SF, 30-Jan-2015.)
Sfin Sfin <fin <fin
 
Theoremsfin111 4536 The finite smaller relationship is one-to-one in its first argument. Theorem X.1.48 of [Rosser] p. 533. (Contributed by SF, 29-Jan-2015.)
Sfin Sfin
 
Theoremspfinex 4537 Spfin is a set. (Contributed by SF, 20-Jan-2015.)
Spfin
 
Theoremncvspfin 4538 The cardinality of the universe is in the finite Sp set. Theorem X.1.49 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
Ncfin Spfin
 
Theoremspfinsfincl 4539 If is in Spfin and is smaller than , then is also in Spfin. Theorem X.1.50 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
Spfin Sfin Spfin
 
Theoremspfininduct 4540* Inductive principle for Spfin. Theorem X.1.51 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
Ncfin Spfin Sfin Spfin
 
Theoremvfinspnn 4541 If the universe is finite, then Spfin is a subset of the nonempty naturals. Theorem X.1.53 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
Fin Spfin Nn
 
Theorem1cvsfin 4542 If the universe is finite, then Ncfin 1c is the base two log of Ncfin . Theorem X.1.54 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
Fin Sfin Ncfin 1c Ncfin
 
Theorem1cspfin 4543 If the universe is finite, then the size of 1c is in Spfin. Corollary of Theorem X.1.54 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
Fin Ncfin 1c Spfin
 
Theoremtncveqnc1fin 4544 If the universe is finite, then the T-raising of the size of the universe is equal to the size of 1c. Theorem X.1.55 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
Fin Tfin Ncfin Ncfin 1c
 
Theoremt1csfin1c 4545 If the universe is finite, then the T-raising of the size of 1c is smaller than the size itself. Corollary of theorem X.1.56 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
Fin Sfin Tfin Ncfin 1c Ncfin 1c
 
Theoremvfintle 4546 If the universe is finite, then the T-raising of all nonempty naturals are no greater than the size of 1c. Theorem X.1.56 of [Rosser] p. 534. (Contributed by SF, 30-Jan-2015.)
Fin Nn Tfin Ncfin 1c <_fin
 
Theoremvfin1cltv 4547 If the universe is finite, then 1c is strictly smaller than the universe. Theorem X.1.57 of [Rosser] p. 534. (Contributed by SF, 30-Jan-2015.)
Fin Ncfin 1c Ncfin <fin
 
Theoremvfinncvntnn 4548 If the universe is finite, then the size of the universe is not the T-raising of a natural. Theorem X.1.58 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
Fin Nn Tfin Ncfin
 
Theoremvfinncvntsp 4549* If the universe is finite, then its size is not a T raising of an element of Spfin. Corollary of theorem X.1.58 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
Fin Ncfin Spfin Tfin
 
Theoremvfinspsslem1 4550* Lemma for vfinspss 4551. Establish part of the inductive step. (Contributed by SF, 3-Feb-2015.)
Fin Tfin Spfin Spfin Sfin Tfin Spfin Tfin
 
Theoremvfinspss 4551* If the universe is finite, then Spfin is a subset of its raisings and the cardinality of the universe. Theorem X.1.59 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)
Fin Spfin Spfin Tfin Ncfin
 
Theoremvfinspclt 4552 If the universe is finite, then Spfin is closed under T-raising. Theorem X.1.60 of [Rosser] p. 536. (Contributed by SF, 30-Jan-2015.)
Fin Spfin Tfin Spfin
 
Theoremvfinspeqtncv 4553* If the universe is finite, then Spfin is equal to its T raisings and the cardinality of the universe. Theorem X.1.61 of [Rosser] p. 536. (Contributed by SF, 29-Jan-2015.)
Fin Spfin Spfin Tfin Ncfin
 
Theoremvfinncsp 4554 If the universe is finite, then the size of Spfin is equal to the successor of its T-raising. Theorem X.1.62 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
Fin Ncfin Spfin Tfin Ncfin Spfin 1c
 
Theoremvinf 4555 The universe is infinite. Theorem X.1.63 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
Fin
 
Theoremnulnnn 4556 The empty class is not a natural. Theorem X.1.65 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
Nn
 
Theorempeano4 4557 The successor operation is one-to-one over the finite cardinals. Theorem X.1.66 of [Rosser] p. 537. (Contributed by SF, 20-Jan-2015.)
Nn Nn 1c 1c
 
Theoremsuc11nnc 4558 Successor cancellation law for finite cardinals. (Contributed by SF, 3-Feb-2015.)
Nn Nn 1c 1c
 
Theoremaddccan2 4559 Cancellation law for natural addition. (Contributed by SF, 3-Feb-2015.)
Nn Nn Nn
 
Theoremaddccan1 4560 Cancellation law for natural addition. (Contributed by SF, 3-Feb-2015.)
Nn Nn Nn
 
2.3  Ordered Pairs, Relationships, and Functions
 
2.3.1  Ordered Pairs
 
Syntaxcop 4561 Declare the syntax for an ordered pair.
 
Syntaxcphi 4562 Declare the syntax for the Phi operation.
Phi
 
Syntaxcproj1 4563 Declare the syntax for the first projection operation.
Proj1
 
Syntaxcproj2 4564 Declare the syntax for the second projection operation.
Proj2
 
Definitiondf-phi 4565* Define the phi operator. This operation increments all the naturals in and leaves all its other members the same. (Contributed by SF, 3-Feb-2015.)
Phi Nn 1c
 
Definitiondf-op 4566* Define the type-level ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
Phi Phi 0c
 
Definitiondf-proj1 4567* Define the first projection operation. This operation recovers the first element of an ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
Proj1 Phi
 
Definitiondf-proj2 4568* Define the second projection operation. This operation recovers the second element of an ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
Proj2 Phi 0c
 
Theoremdfphi2 4569 Express the phi operator in terms of the Kuratowski set construction functions. (Contributed by SF, 3-Feb-2015.)
Phi Imagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k
 
Theoremphieq 4570 Equality law for the Phi operation. (Contributed by SF, 3-Feb-2015.)
Phi Phi
 
Theoremphiexg 4571 The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
Phi
 
Theoremphiex 4572 The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
   =>    Phi
 
Theoremdfop2lem1 4573* Lemma for dfop2 4575 and dfproj22 4577. (Contributed by SF, 2-Jan-2015.)
Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1c Phi 0c
 
Theoremdfop2lem2 4574* Lemma for dfop2 4575 (Contributed by SF, 2-Jan-2015.)
Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck Phi 0c
 
Theoremdfop2 4575 Express the ordered pair via the set construction functors. (Contributed by SF, 2-Jan-2015.)
ImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck
 
Theoremdfproj12 4576 Express the first projection operator via the set construction functors. (Contributed by SF, 2-Jan-2015.)
Proj1 kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k
 
Theoremdfproj22 4577 Express the second projection operator via the set construction functors. (Contributed by SF, 2-Jan-2015.)
Proj2 k Ins2k Sk Ins3k kImagekImagek Ins3k Ins3k Sk Ins2k Sk k1 1 1c Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk k1 1 1 1 1ck1 1 1c Nn k k Nn k k Sk 0c k k1 1 1ck
 
Theoremopeq1 4578 Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
 
Theoremopeq2 4579 Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
 
Theoremopeq12 4580 Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
 
Theoremopeq1i 4581 Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
   =>   
 
Theoremopeq2i 4582 Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
   =>   
 
Theoremopeq12i 4583 Equality inference for ordered pairs. (The proof was shortened by Eric Schmidt, 4-Apr-2007.) (Contributed by SF, 16-Dec-2006.)
   &       =>   
 
Theoremopeq1d 4584 Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
   =>   
 
Theoremopeq2d 4585 Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
   =>   
 
Theoremopeq12d 4586 Equality deduction for ordered pairs. (The proof was shortened by Andrew Salmon, 29-Jun-2011.) (Contributed by SF, 16-Dec-2006.) (Revised by SF, 29-Jun-2011.)
   &       =>   
 
Theoremopexg 4587 An ordered pair of two sets is a set. (Contributed by SF, 2-Jan-2015.)
 
Theoremopex 4588 An ordered pair of two sets is a set. (Contributed by SF, 5-Jan-2015.)
   &       =>   
 
Theoremproj1eq 4589 Equality theorem for first projection operator. (Contributed by SF, 2-Jan-2015.)
Proj1 Proj1
 
Theoremproj2eq 4590 Equality theorem for second projection operator. (Contributed by SF, 2-Jan-2015.)
Proj2 Proj2
 
Theoremproj1exg 4591 The first projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
Proj1
 
Theoremproj2exg 4592 The second projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
Proj2
 
Theoremproj1ex 4593 The first projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
   =>    Proj1
 
Theoremproj2ex 4594 The second projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
   =>    Proj2
 
Theoremphi11lem1 4595 Lemma for phi11 4596. (Contributed by SF, 3-Feb-2015.)
Phi Phi
 
Theoremphi11 4596 The phi operator is one-to-one. Theorem X.2.2 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
Phi Phi
 
Theorem0cnelphi 4597 Cardinal zero is not a member of a phi operation. Theorem X.2.3 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
0c Phi
 
Theoremphi011lem1 4598 Lemma for phi011 4599. (Contributed by SF, 3-Feb-2015.)
Phi 0c Phi 0c Phi Phi
 
Theoremphi011 4599 Phi 0c is one-to-one. Theorem X.2.4 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
Phi 0c Phi 0c
 
Theoremproj1op 4600 The first projection operator applied to an ordered pair yields its first member. Theorem X.2.7 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
Proj1
    < 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 >