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
 
Theoremtfinltfinlem1 4501 Lemma for tfinltfin 4502. Prove the forward direction of the theorem. (Contributed by SF, 2-Feb-2015.)
Nn Nn <fin Tfin Tfin <fin
 
Theoremtfinltfin 4502 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 4503 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 4504 The set of all even naturals exists. (Contributed by SF, 20-Jan-2015.)
Evenfin
 
Theoremoddfinex 4505 The set of all odd naturals exists. (Contributed by SF, 20-Jan-2015.)
Oddfin
 
Theorem0ceven 4506 Cardinal zero is even. (Contributed by SF, 20-Jan-2015.)
0c Evenfin
 
Theoremevennn 4507 An even finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
Evenfin Nn
 
Theoremoddnn 4508 An odd finite cardinal is a finite cardinal. (Contributed by SF, 20-Jan-2015.)
Oddfin Nn
 
Theoremevennnul 4509 An even number is nonempty. (Contributed by SF, 22-Jan-2015.)
Evenfin
 
Theoremoddnnul 4510 An odd number is nonempty. (Contributed by SF, 22-Jan-2015.)
Oddfin
 
Theoremsucevenodd 4511 The successor of an even natural is odd. (Contributed by SF, 20-Jan-2015.)
Evenfin 1c 1c Oddfin
 
Theoremsucoddeven 4512 The successor of an odd natural is even. (Contributed by SF, 22-Jan-2015.)
Oddfin 1c 1c Evenfin
 
Theoremdfevenfin2 4513* Alternate definition of even number. (Contributed by SF, 25-Jan-2015.)
Evenfin Nn
 
Theoremdfoddfin2 4514* Alternate definition of odd number. (Contributed by SF, 25-Jan-2015.)
Oddfin Nn 1c 1c
 
Theoremevenoddnnnul 4515 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 4516* Lemma for evenodddisj 4517. Establish stratification for induction. (Contributed by SF, 25-Jan-2015.)
Nn 1c 1c
 
Theoremevenodddisj 4517 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 4518 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 4519 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 4520* Lemma for nnadjoin 4521. Establish stratification. (Contributed by SF, 29-Jan-2015.)
 
Theoremnnadjoin 4521* 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 4522 Adjoining an element to a power class. Theorem X.1.40 of [Rosser] p. 530. (Contributed by SF, 27-Jan-2015.)
Nn Nn
 
Theoremnnpweqlem1 4523* Lemma for nnpweq 4524. Establish stratification for induction. (Contributed by SF, 26-Jan-2015.)
Nn
 
Theoremnnpweq 4524* 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 4525 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 4526 The expression at the core of srelk 4525 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 4527 Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
Sfin Sfin
 
Theoremsfineq2 4528 Equality theorem for the finite S relationship. (Contributed by SF, 27-Jan-2015.)
Sfin Sfin
 
Theoremsfin01 4529 Zero and one satisfy Sfin. Theorem X.1.42 of [Rosser] p. 530. (Contributed by SF, 30-Jan-2015.)
Sfin 0c 1c
 
Theoremsfin112 4530 Equality law for the finite S operator. Theorem X.1.43 of [Rosser] p. 530. (Contributed by SF, 27-Jan-2015.)
Sfin Sfin
 
Theoremsfindbl 4531* 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 4532* Lemma for sfintfin 4533. Set up induction stratification. (Contributed by SF, 31-Jan-2015.)
Sfin Sfin Tfin Tfin
 
Theoremsfintfin 4533 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 4534* Lemma for tfinnn 4535. Establish stratification. (Contributed by SF, 30-Jan-2015.)
Nn Tfin Tfin
 
Theoremtfinnn 4535* 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 4536 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 4537 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 4538 Spfin is a set. (Contributed by SF, 20-Jan-2015.)
Spfin
 
Theoremncvspfin 4539 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 4540 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 4541* Inductive principle for Spfin. Theorem X.1.51 of [Rosser] p. 534. (Contributed by SF, 27-Jan-2015.)
Ncfin Spfin Sfin Spfin
 
Theoremvfinspnn 4542 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 4543 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 4544 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 4545 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 4546 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 4547 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 4548 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 4549 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 4550* 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 4551* Lemma for vfinspss 4552. Establish part of the inductive step. (Contributed by SF, 3-Feb-2015.)
Fin Tfin Spfin Spfin Sfin Tfin Spfin Tfin
 
Theoremvfinspss 4552* 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 4553 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 4554* 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 4555 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 4556 The universe is infinite. Theorem X.1.63 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
Fin
 
Theoremnulnnn 4557 The empty class is not a natural. Theorem X.1.65 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)
Nn
 
Theorempeano4 4558 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 4559 Successor cancellation law for finite cardinals. (Contributed by SF, 3-Feb-2015.)
Nn Nn 1c 1c
 
Theoremaddccan2 4560 Cancellation law for natural addition. (Contributed by SF, 3-Feb-2015.)
Nn Nn Nn
 
Theoremaddccan1 4561 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 4562 Declare the syntax for an ordered pair.
 
Syntaxcphi 4563 Declare the syntax for the Phi operation.
Phi
 
Syntaxcproj1 4564 Declare the syntax for the first projection operation.
Proj1
 
Syntaxcproj2 4565 Declare the syntax for the second projection operation.
Proj2
 
Definitiondf-phi 4566* 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 4567* Define the type-level ordered pair. Definition from [Rosser] p. 281. (Contributed by SF, 3-Feb-2015.)
Phi Phi 0c
 
Definitiondf-proj1 4568* 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 4569* 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 4570 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 4571 Equality law for the Phi operation. (Contributed by SF, 3-Feb-2015.)
Phi Phi
 
Theoremphiexg 4572 The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
Phi
 
Theoremphiex 4573 The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
   =>    Phi
 
Theoremdfop2lem1 4574* Lemma for dfop2 4576 and dfproj22 4578. (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 4575* Lemma for dfop2 4576. (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 4576 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 4577 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 4578 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 4579 Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
 
Theoremopeq2 4580 Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
 
Theoremopeq12 4581 Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
 
Theoremopeq1i 4582 Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
   =>   
 
Theoremopeq2i 4583 Equality inference for ordered pairs. (Contributed by SF, 16-Dec-2006.)
   =>   
 
Theoremopeq12i 4584 Equality inference for ordered pairs. (The proof was shortened by Eric Schmidt, 4-Apr-2007.) (Contributed by SF, 16-Dec-2006.)
   &       =>   
 
Theoremopeq1d 4585 Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
   =>   
 
Theoremopeq2d 4586 Equality deduction for ordered pairs. (Contributed by SF, 16-Dec-2006.)
   =>   
 
Theoremopeq12d 4587 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 4588 An ordered pair of two sets is a set. (Contributed by SF, 2-Jan-2015.)
 
Theoremopex 4589 An ordered pair of two sets is a set. (Contributed by SF, 5-Jan-2015.)
   &       =>   
 
Theoremproj1eq 4590 Equality theorem for first projection operator. (Contributed by SF, 2-Jan-2015.)
Proj1 Proj1
 
Theoremproj2eq 4591 Equality theorem for second projection operator. (Contributed by SF, 2-Jan-2015.)
Proj2 Proj2
 
Theoremproj1exg 4592 The first projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
Proj1
 
Theoremproj2exg 4593 The second projection of a set is a set. (Contributed by SF, 2-Jan-2015.)
Proj2
 
Theoremproj1ex 4594 The first projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
   =>    Proj1
 
Theoremproj2ex 4595 The second projection of a set is a set. (Contributed by Scott Fenton, 16-Apr-2021.)
   =>    Proj2
 
Theoremphi11lem1 4596 Lemma for phi11 4597. (Contributed by SF, 3-Feb-2015.)
Phi Phi
 
Theoremphi11 4597 The phi operator is one-to-one. Theorem X.2.2 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
Phi Phi
 
Theorem0cnelphi 4598 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 4599 Lemma for phi011 4600. (Contributed by SF, 3-Feb-2015.)
Phi 0c Phi 0c Phi Phi
 
Theoremphi011 4600 Phi 0c is one-to-one. Theorem X.2.4 of [Rosser] p. 282. (Contributed by SF, 3-Feb-2015.)
Phi 0c Phi 0c
    < 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-6339
  Copyright terms: Public domain < Previous  Next >