Type  Label  Description 
Statement 

Theorem  tfinltfin 4501 
Ordering rule for the finite T operation. Corollary to theorem X.1.33
of [Rosser] p. 529. (Contributed by SF,
1Feb2015.)

Nn Nn _{fin} T_{fin} T_{fin} _{fin} 

Theorem  tfinlefin 4502 
Ordering rule for the finite T operation. Theorem X.1.33 of [Rosser]
p. 529. (Contributed by SF, 2Feb2015.)

Nn Nn _{fin} T_{fin} T_{fin} _{fin} 

Theorem  evenfinex 4503 
The set of all even naturals exists. (Contributed by SF,
20Jan2015.)

Even_{fin} 

Theorem  oddfinex 4504 
The set of all odd naturals exists. (Contributed by SF,
20Jan2015.)

Odd_{fin}


Theorem  0ceven 4505 
Cardinal zero is even. (Contributed by SF, 20Jan2015.)

0_{c} Even_{fin} 

Theorem  evennn 4506 
An even finite cardinal is a finite cardinal. (Contributed by SF,
20Jan2015.)

Even_{fin} Nn 

Theorem  oddnn 4507 
An odd finite cardinal is a finite cardinal. (Contributed by SF,
20Jan2015.)

Odd_{fin} Nn 

Theorem  evennnul 4508 
An even number is nonempty. (Contributed by SF, 22Jan2015.)

Even_{fin} 

Theorem  oddnnul 4509 
An odd number is nonempty. (Contributed by SF, 22Jan2015.)

Odd_{fin} 

Theorem  sucevenodd 4510 
The successor of an even natural is odd. (Contributed by SF,
20Jan2015.)

Even_{fin}
1_{c}
1_{c}
Odd_{fin} 

Theorem  sucoddeven 4511 
The successor of an odd natural is even. (Contributed by SF,
22Jan2015.)

Odd_{fin}
1_{c}
1_{c}
Even_{fin} 

Theorem  dfevenfin2 4512* 
Alternate definition of even number. (Contributed by SF,
25Jan2015.)

Even_{fin} Nn


Theorem  dfoddfin2 4513* 
Alternate definition of odd number. (Contributed by SF,
25Jan2015.)

Odd_{fin}
Nn 1_{c} 1_{c} 

Theorem  evenoddnnnul 4514 
Every nonempty finite cardinal is either even or odd. Theorem X.1.35 of
[Rosser] p. 529. (Contributed by SF,
20Jan2015.)

Even_{fin} Odd_{fin}
Nn 

Theorem  evenodddisjlem1 4515* 
Lemma for evenodddisj 4516. Establish stratification for induction.
(Contributed by SF, 25Jan2015.)

Nn 1_{c}
1_{c} 

Theorem  evenodddisj 4516 
The even finite cardinals and the odd ones are disjoint. Theorem X.1.36
of [Rosser] p. 529. (Contributed by SF,
22Jan2015.)

Even_{fin} Odd_{fin}


Theorem  eventfin 4517 
If is even , then so
is T_{fin} . Theorem X.1.37 of
[Rosser] p. 530. (Contributed by SF,
26Jan2015.)

Even_{fin} T_{fin} Even_{fin} 

Theorem  oddtfin 4518 
If is odd , then so
is T_{fin} . Theorem X.1.38 of [Rosser]
p. 530. (Contributed by SF, 26Jan2015.)

Odd_{fin} T_{fin} Odd_{fin} 

Theorem  nnadjoinlem1 4519* 
Lemma for nnadjoin 4520. Establish stratification. (Contributed by
SF,
29Jan2015.)

∼


Theorem  nnadjoin 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,
29Jan2015.)

Nn ∼


Theorem  nnadjoinpw 4521 
Adjoining an element to a power class. Theorem X.1.40 of [Rosser]
p. 530. (Contributed by SF, 27Jan2015.)

Nn Nn ∼


Theorem  nnpweqlem1 4522* 
Lemma for nnpweq 4523. Establish stratification for induction.
(Contributed by SF, 26Jan2015.)

Nn 

Theorem  nnpweq 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, 26Jan2015.)

Nn
Nn 

Theorem  srelk 4524 
Binary relationship form of the S_{fin}
relationship. (Contributed
by SF, 23Jan2015.)

Nn _{k} Nn
Ins3_{k} Ins3_{k} SI_{k} 1_{c} _{k}
Ins3_{k} S_{k} Ins2_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} 1_{c} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k}
Ins3_{k} SI_{k} ∼ Ins3_{k} S_{k} Ins2_{k} SI_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k}
S_{k} _{k}_{1} _{1} 1_{c}_{k}_{1} _{1} _{1} 1_{c}
S_{fin} 

Theorem  srelkex 4525 
The expression at the core of srelk 4524 exists. (Contributed by SF,
30Jan2015.)

Nn _{k} Nn
Ins3_{k} Ins3_{k} SI_{k} 1_{c} _{k}
Ins3_{k} S_{k} Ins2_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} 1_{c} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k}
Ins3_{k} SI_{k} ∼ Ins3_{k} S_{k} Ins2_{k} SI_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k}
S_{k} _{k}_{1} _{1} 1_{c}_{k}_{1} _{1} _{1} 1_{c}


Theorem  sfineq1 4526 
Equality theorem for the finite S relationship. (Contributed by SF,
27Jan2015.)

S_{fin} S_{fin} 

Theorem  sfineq2 4527 
Equality theorem for the finite S relationship. (Contributed by SF,
27Jan2015.)

S_{fin} S_{fin} 

Theorem  sfin01 4528 
Zero and one satisfy S_{fin}. Theorem
X.1.42 of [Rosser] p. 530.
(Contributed by SF, 30Jan2015.)

S_{fin}
0_{c} 1_{c} 

Theorem  sfin112 4529 
Equality law for the finite S operator. Theorem X.1.43 of [Rosser]
p. 530. (Contributed by SF, 27Jan2015.)

S_{fin} S_{fin} 

Theorem  sfindbl 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, 30Jan2015.)

Nn _{1}
1_{c} Nn S_{fin} S_{fin}
1_{c} 

Theorem  sfintfinlem1 4531* 
Lemma for sfintfin 4532. Set up induction stratification.
(Contributed
by SF, 31Jan2015.)

S_{fin} S_{fin} T_{fin} T_{fin} 

Theorem  sfintfin 4532 
If two numbers obey S_{fin}, then do their
T raisings. Theorem
X.1.45 of [Rosser] p. 532. (Contributed
by SF, 30Jan2015.)

S_{fin} S_{fin} T_{fin} T_{fin} 

Theorem  tfinnnlem1 4533* 
Lemma for tfinnn 4534. Establish stratification. (Contributed by
SF,
30Jan2015.)

Nn
T_{fin} T_{fin} 

Theorem  tfinnn 4534* 
Traising of a set of naturals. Theorem X.1.46 of [Rosser] p. 532.
(Contributed by SF, 30Jan2015.)

Nn Nn
T_{fin} T_{fin} 

Theorem  sfinltfin 4535 
Ordering law for finite smaller than. Theorem X.1.47 of [Rosser]
p. 532. (Contributed by SF, 30Jan2015.)

S_{fin} S_{fin} _{fin} _{fin} 

Theorem  sfin111 4536 
The finite smaller relationship is onetoone in its first argument.
Theorem X.1.48 of [Rosser] p. 533.
(Contributed by SF, 29Jan2015.)

S_{fin} S_{fin} 

Theorem  spfinex 4537 
Sp_{fin} is a set. (Contributed by SF,
20Jan2015.)

Sp_{fin}


Theorem  ncvspfin 4538 
The cardinality of the universe is in the finite Sp set. Theorem X.1.49
of [Rosser] p. 534. (Contributed by SF,
27Jan2015.)

Nc_{fin}
Sp_{fin} 

Theorem  spfinsfincl 4539 
If is in Sp_{fin} and is smaller than , then
is also in Sp_{fin}. Theorem
X.1.50 of [Rosser] p. 534.
(Contributed by SF, 27Jan2015.)

Sp_{fin} S_{fin}
Sp_{fin} 

Theorem  spfininduct 4540* 
Inductive principle for Sp_{fin}. Theorem
X.1.51 of [Rosser]
p. 534. (Contributed by SF, 27Jan2015.)

Nc_{fin} Sp_{fin} S_{fin}
Sp_{fin} 

Theorem  vfinspnn 4541 
If the universe is finite, then Sp_{fin}
is a subset of the nonempty
naturals. Theorem X.1.53 of [Rosser] p.
534. (Contributed by SF,
27Jan2015.)

Fin Sp_{fin} Nn 

Theorem  1cvsfin 4542 
If the universe is finite, then Nc_{fin}
1_{c} is the base two log of
Nc_{fin} . Theorem X.1.54 of [Rosser] p. 534. (Contributed by SF,
29Jan2015.)

Fin S_{fin} Nc_{fin} 1_{c} Nc_{fin} 

Theorem  1cspfin 4543 
If the universe is finite, then the size of 1_{c} is in Sp_{fin}.
Corollary of Theorem X.1.54 of [Rosser] p.
534. (Contributed by SF,
29Jan2015.)

Fin Nc_{fin} 1_{c}
Sp_{fin} 

Theorem  tncveqnc1fin 4544 
If the universe is finite, then the Traising of the size of the universe
is equal to the size of 1_{c}. Theorem X.1.55 of [Rosser] p. 534.
(Contributed by SF, 29Jan2015.)

Fin T_{fin} Nc_{fin} Nc_{fin}
1_{c} 

Theorem  t1csfin1c 4545 
If the universe is finite, then the Traising of the size of
1_{c} is
smaller than the size itself. Corollary of theorem X.1.56 of [Rosser]
p. 534. (Contributed by SF, 29Jan2015.)

Fin S_{fin} T_{fin} Nc_{fin} 1_{c} Nc_{fin} 1_{c} 

Theorem  vfintle 4546 
If the universe is finite, then the Traising of all nonempty naturals
are no greater than the size of 1_{c}. Theorem X.1.56 of
[Rosser]
p. 534. (Contributed by SF, 30Jan2015.)

Fin Nn T_{fin} Nc_{fin}
1_{c} _{fin} 

Theorem  vfin1cltv 4547 
If the universe is finite, then 1_{c} is strictly smaller than
the
universe. Theorem X.1.57 of [Rosser] p.
534. (Contributed by SF,
30Jan2015.)

Fin Nc_{fin}
1_{c} Nc_{fin} _{fin} 

Theorem  vfinncvntnn 4548 
If the universe is finite, then the size of the universe is not the
Traising of a natural. Theorem X.1.58 of [Rosser] p. 534.
(Contributed by SF, 29Jan2015.)

Fin Nn T_{fin} Nc_{fin} 

Theorem  vfinncvntsp 4549* 
If the universe is finite, then its size is not a T raising of an
element of Sp_{fin}. Corollary of
theorem X.1.58 of [Rosser]
p. 534. (Contributed by SF, 27Jan2015.)

Fin Nc_{fin}
Sp_{fin}
T_{fin} 

Theorem  vfinspsslem1 4550* 
Lemma for vfinspss 4551. Establish part of the inductive step.
(Contributed by SF, 3Feb2015.)

Fin T_{fin} Sp_{fin} Sp_{fin} S_{fin}
T_{fin} Sp_{fin} T_{fin} 

Theorem  vfinspss 4551* 
If the universe is finite, then Sp_{fin}
is a subset of its
raisings and the cardinality of the universe. Theorem X.1.59 of
[Rosser] p. 534. (Contributed by SF,
29Jan2015.)

Fin Sp_{fin}
Sp_{fin} T_{fin}
Nc_{fin} 

Theorem  vfinspclt 4552 
If the universe is finite, then Sp_{fin}
is closed under Traising.
Theorem X.1.60 of [Rosser] p. 536.
(Contributed by SF, 30Jan2015.)

Fin Sp_{fin} T_{fin} Sp_{fin} 

Theorem  vfinspeqtncv 4553* 
If the universe is finite, then Sp_{fin}
is equal to its T raisings
and the cardinality of the universe. Theorem X.1.61 of [Rosser] p. 536.
(Contributed by SF, 29Jan2015.)

Fin Sp_{fin} Sp_{fin} T_{fin} Nc_{fin} 

Theorem  vfinncsp 4554 
If the universe is finite, then the size of Sp_{fin} is equal to the
successor of its Traising. Theorem X.1.62 of [Rosser] p. 536.
(Contributed by SF, 20Jan2015.)

Fin Nc_{fin} Sp_{fin}
T_{fin} Nc_{fin} Sp_{fin} 1_{c} 

Theorem  vinf 4555 
The universe is infinite. Theorem X.1.63 of [Rosser] p. 536.
(Contributed by SF, 20Jan2015.)

Fin 

Theorem  nulnnn 4556 
The empty class is not a natural. Theorem X.1.65 of [Rosser] p. 536.
(Contributed by SF, 20Jan2015.)

Nn 

Theorem  peano4 4557 
The successor operation is onetoone over the finite cardinals. Theorem
X.1.66 of [Rosser] p. 537. (Contributed by
SF, 20Jan2015.)

Nn Nn
1_{c}
1_{c} 

Theorem  suc11nnc 4558 
Successor cancellation law for finite cardinals. (Contributed by SF,
3Feb2015.)

Nn Nn 1_{c}
1_{c}


Theorem  addccan2 4559 
Cancellation law for natural addition. (Contributed by SF,
3Feb2015.)

Nn Nn Nn


Theorem  addccan1 4560 
Cancellation law for natural addition. (Contributed by SF,
3Feb2015.)

Nn Nn Nn


2.3 Ordered Pairs, Relationships, and
Functions


2.3.1 Ordered Pairs


Syntax  cop 4561 
Declare the syntax for an ordered pair.



Syntax  cphi 4562 
Declare the syntax for the Phi operation.

Phi 

Syntax  cproj1 4563 
Declare the syntax for the first projection operation.

Proj1 

Syntax  cproj2 4564 
Declare the syntax for the second projection operation.

Proj2 

Definition  dfphi 4565* 
Define the phi operator. This operation increments all the naturals in
and leaves
all its other members the same. (Contributed by SF,
3Feb2015.)

Phi
Nn 1_{c} 

Definition  dfop 4566* 
Define the typelevel ordered pair. Definition from [Rosser] p. 281.
(Contributed by SF, 3Feb2015.)

Phi
Phi 0_{c} 

Definition  dfproj1 4567* 
Define the first projection operation. This operation recovers the
first element of an ordered pair. Definition from [Rosser] p. 281.
(Contributed by SF, 3Feb2015.)

Proj1 Phi 

Definition  dfproj2 4568* 
Define the second projection operation. This operation recovers the
second element of an ordered pair. Definition from [Rosser] p. 281.
(Contributed by SF, 3Feb2015.)

Proj2 Phi
0_{c} 

Theorem  dfphi2 4569 
Express the phi operator in terms of the Kuratowski set construction
functions. (Contributed by SF, 3Feb2015.)

Phi Image_{k}
Ins3_{k} ∼ Ins3_{k}
S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c}_{k}_{1} _{1} 1_{c} Nn _{k} _{k} ∼ Nn _{k} _{k} 

Theorem  phieq 4570 
Equality law for the Phi operation. (Contributed by SF, 3Feb2015.)

Phi Phi 

Theorem  phiexg 4571 
The phi operator preserves sethood. (Contributed by SF, 3Feb2015.)

Phi 

Theorem  phiex 4572 
The phi operator preserves sethood. (Contributed by SF, 3Feb2015.)

Phi 

Theorem  dfop2lem1 4573* 
Lemma for dfop2 4575 and dfproj22 4577. (Contributed by SF, 2Jan2015.)

∼ Ins2_{k} S_{k} Ins3_{k} _{k}Image_{k}Image_{k}
Ins3_{k} ∼ Ins3_{k}
S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c}_{k}_{1} _{1} 1_{c} Nn _{k} _{k} ∼ Nn _{k} _{k} S_{k} 0_{c} _{k} _{k}_{1} _{1} 1_{c} Phi 0_{c} 

Theorem  dfop2lem2 4574* 
Lemma for dfop2 4575 (Contributed by SF, 2Jan2015.)

∼ Ins2_{k} S_{k} Ins3_{k} _{k}Image_{k}Image_{k}
Ins3_{k} ∼ Ins3_{k}
S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c}_{k}_{1} _{1} 1_{c} Nn _{k} _{k} ∼ Nn _{k} _{k} S_{k} 0_{c} _{k} _{k}_{1} _{1} 1_{c}_{k}
Phi 0_{c} 

Theorem  dfop2 4575 
Express the ordered pair via the set construction functors.
(Contributed by SF, 2Jan2015.)

Image_{k}Image_{k}
Ins3_{k} ∼ Ins3_{k}
S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c}_{k}_{1} _{1} 1_{c} Nn _{k} _{k} ∼ Nn _{k} _{k} ∼ Ins2_{k} S_{k} Ins3_{k} _{k}Image_{k}Image_{k}
Ins3_{k} ∼ Ins3_{k}
S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c}_{k}_{1} _{1} 1_{c} Nn _{k} _{k} ∼ Nn _{k} _{k} S_{k} 0_{c} _{k} _{k}_{1} _{1} 1_{c}_{k} 

Theorem  dfproj12 4576 
Express the first projection operator via the set construction functors.
(Contributed by SF, 2Jan2015.)

Proj1 _{k}Image_{k}Image_{k}
Ins3_{k} ∼ Ins3_{k}
S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c}_{k}_{1} _{1} 1_{c} Nn _{k} _{k} ∼ Nn _{k} _{k} 

Theorem  dfproj22 4577 
Express the second projection operator via the set construction
functors. (Contributed by SF, 2Jan2015.)

Proj2 _{k} ∼
Ins2_{k} S_{k} Ins3_{k} _{k}Image_{k}Image_{k}
Ins3_{k} ∼ Ins3_{k}
S_{k} Ins2_{k} S_{k} _{k}_{1} _{1} 1_{c} Ins2_{k} Ins2_{k} S_{k} Ins2_{k} Ins3_{k} S_{k} Ins3_{k} SI_{k} SI_{k} S_{k} _{k}_{1} _{1} _{1} _{1} 1_{c}_{k}_{1} _{1} 1_{c} Nn _{k} _{k} ∼ Nn _{k} _{k} S_{k} 0_{c} _{k} _{k}_{1} _{1} 1_{c}_{k} 

Theorem  opeq1 4578 
Equality theorem for ordered pairs. (Contributed by SF, 2Jan2015.)



Theorem  opeq2 4579 
Equality theorem for ordered pairs. (Contributed by SF, 2Jan2015.)



Theorem  opeq12 4580 
Equality theorem for ordered pairs. (Contributed by SF, 2Jan2015.)



Theorem  opeq1i 4581 
Equality inference for ordered pairs. (Contributed by SF,
16Dec2006.)



Theorem  opeq2i 4582 
Equality inference for ordered pairs. (Contributed by SF,
16Dec2006.)



Theorem  opeq12i 4583 
Equality inference for ordered pairs. (The proof was shortened by
Eric Schmidt, 4Apr2007.) (Contributed by SF, 16Dec2006.)



Theorem  opeq1d 4584 
Equality deduction for ordered pairs. (Contributed by SF,
16Dec2006.)



Theorem  opeq2d 4585 
Equality deduction for ordered pairs. (Contributed by SF,
16Dec2006.)



Theorem  opeq12d 4586 
Equality deduction for ordered pairs. (The proof was shortened by
Andrew Salmon, 29Jun2011.) (Contributed by SF, 16Dec2006.)
(Revised by SF, 29Jun2011.)



Theorem  opexg 4587 
An ordered pair of two sets is a set. (Contributed by SF, 2Jan2015.)



Theorem  opex 4588 
An ordered pair of two sets is a set. (Contributed by SF,
5Jan2015.)



Theorem  proj1eq 4589 
Equality theorem for first projection operator. (Contributed by SF,
2Jan2015.)

Proj1 Proj1


Theorem  proj2eq 4590 
Equality theorem for second projection operator. (Contributed by SF,
2Jan2015.)

Proj2 Proj2


Theorem  proj1exg 4591 
The first projection of a set is a set. (Contributed by SF,
2Jan2015.)

Proj1 

Theorem  proj2exg 4592 
The second projection of a set is a set. (Contributed by SF,
2Jan2015.)

Proj2 

Theorem  proj1ex 4593 
The first projection of a set is a set. (Contributed by Scott Fenton,
16Apr2021.)

Proj1 

Theorem  proj2ex 4594 
The second projection of a set is a set. (Contributed by Scott Fenton,
16Apr2021.)

Proj2 

Theorem  phi11lem1 4595 
Lemma for phi11 4596. (Contributed by SF, 3Feb2015.)

Phi Phi


Theorem  phi11 4596 
The phi operator is onetoone. Theorem X.2.2 of [Rosser] p. 282.
(Contributed by SF, 3Feb2015.)

Phi Phi 

Theorem  0cnelphi 4597 
Cardinal zero is not a member of a phi operation. Theorem X.2.3 of
[Rosser] p. 282. (Contributed by SF,
3Feb2015.)

0_{c} Phi 

Theorem  phi011lem1 4598 
Lemma for phi011 4599. (Contributed by SF, 3Feb2015.)

Phi 0_{c}
Phi 0_{c} Phi Phi 

Theorem  phi011 4599 
Phi 0_{c} is onetoone. Theorem X.2.4 of [Rosser] p. 282.
(Contributed by SF, 3Feb2015.)

Phi 0_{c}
Phi 0_{c} 

Theorem  proj1op 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,
3Feb2015.)

Proj1
