Theorem List for New Foundations Explorer - 4501-4600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | tfinltfinlem1 4501 |
Lemma for tfinltfin 4502. Prove the forward direction of the theorem.
(Contributed by SF, 2-Feb-2015.)
|
Nn Nn fin Tfin Tfin fin |
|
Theorem | tfinltfin 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 |
|
Theorem | tfinlefin 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 |
|
Theorem | evenfinex 4504 |
The set of all even naturals exists. (Contributed by SF,
20-Jan-2015.)
|
Evenfin |
|
Theorem | oddfinex 4505 |
The set of all odd naturals exists. (Contributed by SF,
20-Jan-2015.)
|
Oddfin
|
|
Theorem | 0ceven 4506 |
Cardinal zero is even. (Contributed by SF, 20-Jan-2015.)
|
0c Evenfin |
|
Theorem | evennn 4507 |
An even finite cardinal is a finite cardinal. (Contributed by SF,
20-Jan-2015.)
|
Evenfin Nn |
|
Theorem | oddnn 4508 |
An odd finite cardinal is a finite cardinal. (Contributed by SF,
20-Jan-2015.)
|
Oddfin Nn |
|
Theorem | evennnul 4509 |
An even number is nonempty. (Contributed by SF, 22-Jan-2015.)
|
Evenfin |
|
Theorem | oddnnul 4510 |
An odd number is nonempty. (Contributed by SF, 22-Jan-2015.)
|
Oddfin |
|
Theorem | sucevenodd 4511 |
The successor of an even natural is odd. (Contributed by SF,
20-Jan-2015.)
|
Evenfin
1c
1c
Oddfin |
|
Theorem | sucoddeven 4512 |
The successor of an odd natural is even. (Contributed by SF,
22-Jan-2015.)
|
Oddfin
1c
1c
Evenfin |
|
Theorem | dfevenfin2 4513* |
Alternate definition of even number. (Contributed by SF,
25-Jan-2015.)
|
Evenfin Nn
|
|
Theorem | dfoddfin2 4514* |
Alternate definition of odd number. (Contributed by SF,
25-Jan-2015.)
|
Oddfin
Nn 1c 1c |
|
Theorem | evenoddnnnul 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 |
|
Theorem | evenodddisjlem1 4516* |
Lemma for evenodddisj 4517. Establish stratification for induction.
(Contributed by SF, 25-Jan-2015.)
|
Nn 1c
1c |
|
Theorem | evenodddisj 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
|
|
Theorem | eventfin 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 |
|
Theorem | oddtfin 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 |
|
Theorem | nnadjoinlem1 4520* |
Lemma for nnadjoin 4521. Establish stratification. (Contributed by
SF,
29-Jan-2015.)
|
∼
|
|
Theorem | nnadjoin 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 ∼
|
|
Theorem | nnadjoinpw 4522 |
Adjoining an element to a power class. Theorem X.1.40 of [Rosser]
p. 530. (Contributed by SF, 27-Jan-2015.)
|
Nn Nn ∼
|
|
Theorem | nnpweqlem1 4523* |
Lemma for nnpweq 4524. Establish stratification for induction.
(Contributed by SF, 26-Jan-2015.)
|
Nn |
|
Theorem | nnpweq 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 |
|
Theorem | srelk 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 |
|
Theorem | srelkex 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
|
|
Theorem | sfineq1 4527 |
Equality theorem for the finite S relationship. (Contributed by SF,
27-Jan-2015.)
|
Sfin Sfin |
|
Theorem | sfineq2 4528 |
Equality theorem for the finite S relationship. (Contributed by SF,
27-Jan-2015.)
|
Sfin Sfin |
|
Theorem | sfin01 4529 |
Zero and one satisfy Sfin. Theorem
X.1.42 of [Rosser] p. 530.
(Contributed by SF, 30-Jan-2015.)
|
Sfin
0c 1c |
|
Theorem | sfin112 4530 |
Equality law for the finite S operator. Theorem X.1.43 of [Rosser]
p. 530. (Contributed by SF, 27-Jan-2015.)
|
Sfin Sfin |
|
Theorem | sfindbl 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 |
|
Theorem | sfintfinlem1 4532* |
Lemma for sfintfin 4533. Set up induction stratification.
(Contributed
by SF, 31-Jan-2015.)
|
Sfin Sfin Tfin Tfin |
|
Theorem | sfintfin 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 |
|
Theorem | tfinnnlem1 4534* |
Lemma for tfinnn 4535. Establish stratification. (Contributed by
SF,
30-Jan-2015.)
|
Nn
Tfin Tfin |
|
Theorem | tfinnn 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 |
|
Theorem | sfinltfin 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 |
|
Theorem | sfin111 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 |
|
Theorem | spfinex 4538 |
Spfin is a set. (Contributed by SF,
20-Jan-2015.)
|
Spfin
|
|
Theorem | ncvspfin 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 |
|
Theorem | spfinsfincl 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 |
|
Theorem | spfininduct 4541* |
Inductive principle for Spfin. Theorem
X.1.51 of [Rosser]
p. 534. (Contributed by SF, 27-Jan-2015.)
|
Ncfin Spfin Sfin
Spfin |
|
Theorem | vfinspnn 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 |
|
Theorem | 1cvsfin 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 |
|
Theorem | 1cspfin 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 |
|
Theorem | tncveqnc1fin 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 |
|
Theorem | t1csfin1c 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 |
|
Theorem | vfintle 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 |
|
Theorem | vfin1cltv 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 |
|
Theorem | vfinncvntnn 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 |
|
Theorem | vfinncvntsp 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 |
|
Theorem | vfinspsslem1 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 |
|
Theorem | vfinspss 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 |
|
Theorem | vfinspclt 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 |
|
Theorem | vfinspeqtncv 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 |
|
Theorem | vfinncsp 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 |
|
Theorem | vinf 4556 |
The universe is infinite. Theorem X.1.63 of [Rosser] p. 536.
(Contributed by SF, 20-Jan-2015.)
|
Fin |
|
Theorem | nulnnn 4557 |
The empty class is not a natural. Theorem X.1.65 of [Rosser] p. 536.
(Contributed by SF, 20-Jan-2015.)
|
Nn |
|
Theorem | peano4 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 |
|
Theorem | suc11nnc 4559 |
Successor cancellation law for finite cardinals. (Contributed by SF,
3-Feb-2015.)
|
Nn Nn 1c
1c
|
|
Theorem | addccan2 4560 |
Cancellation law for natural addition. (Contributed by SF,
3-Feb-2015.)
|
Nn Nn Nn
|
|
Theorem | addccan1 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
|
|
Syntax | cop 4562 |
Declare the syntax for an ordered pair.
|
|
|
Syntax | cphi 4563 |
Declare the syntax for the Phi operation.
|
Phi |
|
Syntax | cproj1 4564 |
Declare the syntax for the first projection operation.
|
Proj1 |
|
Syntax | cproj2 4565 |
Declare the syntax for the second projection operation.
|
Proj2 |
|
Definition | df-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 |
|
Definition | df-op 4567* |
Define the type-level ordered pair. Definition from [Rosser] p. 281.
(Contributed by SF, 3-Feb-2015.)
|
Phi
Phi 0c |
|
Definition | df-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 |
|
Definition | df-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 |
|
Theorem | dfphi2 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 |
|
Theorem | phieq 4571 |
Equality law for the Phi operation. (Contributed by SF, 3-Feb-2015.)
|
Phi Phi |
|
Theorem | phiexg 4572 |
The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
|
Phi |
|
Theorem | phiex 4573 |
The phi operator preserves sethood. (Contributed by SF, 3-Feb-2015.)
|
Phi |
|
Theorem | dfop2lem1 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 |
|
Theorem | dfop2lem2 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 |
|
Theorem | dfop2 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 |
|
Theorem | dfproj12 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 |
|
Theorem | dfproj22 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 |
|
Theorem | opeq1 4579 |
Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|
|
|
Theorem | opeq2 4580 |
Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|
|
|
Theorem | opeq12 4581 |
Equality theorem for ordered pairs. (Contributed by SF, 2-Jan-2015.)
|
|
|
Theorem | opeq1i 4582 |
Equality inference for ordered pairs. (Contributed by SF,
16-Dec-2006.)
|
|
|
Theorem | opeq2i 4583 |
Equality inference for ordered pairs. (Contributed by SF,
16-Dec-2006.)
|
|
|
Theorem | opeq12i 4584 |
Equality inference for ordered pairs. (The proof was shortened by
Eric Schmidt, 4-Apr-2007.) (Contributed by SF, 16-Dec-2006.)
|
|
|
Theorem | opeq1d 4585 |
Equality deduction for ordered pairs. (Contributed by SF,
16-Dec-2006.)
|
|
|
Theorem | opeq2d 4586 |
Equality deduction for ordered pairs. (Contributed by SF,
16-Dec-2006.)
|
|
|
Theorem | opeq12d 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.)
|
|
|
Theorem | opexg 4588 |
An ordered pair of two sets is a set. (Contributed by SF, 2-Jan-2015.)
|
|
|
Theorem | opex 4589 |
An ordered pair of two sets is a set. (Contributed by SF,
5-Jan-2015.)
|
|
|
Theorem | proj1eq 4590 |
Equality theorem for first projection operator. (Contributed by SF,
2-Jan-2015.)
|
Proj1 Proj1
|
|
Theorem | proj2eq 4591 |
Equality theorem for second projection operator. (Contributed by SF,
2-Jan-2015.)
|
Proj2 Proj2
|
|
Theorem | proj1exg 4592 |
The first projection of a set is a set. (Contributed by SF,
2-Jan-2015.)
|
Proj1 |
|
Theorem | proj2exg 4593 |
The second projection of a set is a set. (Contributed by SF,
2-Jan-2015.)
|
Proj2 |
|
Theorem | proj1ex 4594 |
The first projection of a set is a set. (Contributed by Scott Fenton,
16-Apr-2021.)
|
Proj1 |
|
Theorem | proj2ex 4595 |
The second projection of a set is a set. (Contributed by Scott Fenton,
16-Apr-2021.)
|
Proj2 |
|
Theorem | phi11lem1 4596 |
Lemma for phi11 4597. (Contributed by SF, 3-Feb-2015.)
|
Phi Phi
|
|
Theorem | phi11 4597 |
The phi operator is one-to-one. Theorem X.2.2 of [Rosser] p. 282.
(Contributed by SF, 3-Feb-2015.)
|
Phi Phi |
|
Theorem | 0cnelphi 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 |
|
Theorem | phi011lem1 4599 |
Lemma for phi011 4600. (Contributed by SF, 3-Feb-2015.)
|
Phi 0c
Phi 0c Phi Phi |
|
Theorem | phi011 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 |