Home New Foundations ExplorerTheorem 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 non-empty. (Contributed by SF, 22-Jan-2015.)
Evenfin

Theoremoddnnul 4509 An odd number is non-empty. (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 non-empty 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 non-empty 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 non-empty 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

Nn Nn Nn

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

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 >