Type  Label  Description 
Statement 

Theorem  0cnsuc 4401 
Cardinal zero is not a successor. Compare Theorem X.1.2 of [Rosser]
p. 275. (Contributed by SF, 14Jan2015.)

1_{c}
0_{c} 

Theorem  peano1 4402 
Cardinal zero is a finite cardinal. Theorem X.1.4 of [Rosser] p. 276.
(Contributed by SF, 14Jan2015.)

0_{c} Nn 

Theorem  peano2 4403 
The finite cardinals are closed under addition of one. Theorem X.1.5 of
[Rosser] p. 276. (Contributed by SF,
14Jan2015.)

Nn 1_{c} Nn 

Theorem  peano3 4404 
The successor of a finite cardinal is not zero. (Contributed by SF,
14Jan2015.)

Nn 1_{c} 0_{c} 

Theorem  addcid1 4405 
Cardinal zero is a fixed point for cardinal addition. Theorem X.1.8 of
[Rosser] p. 276. (Contributed by SF,
16Jan2015.)

0_{c}


Theorem  addccom 4406 
Cardinal sum commutes. Theorem X.1.9 of [Rosser] p. 276. (Contributed
by SF, 15Jan2015.)



Theorem  addcid2 4407 
Cardinal zero is a fixed point for cardinal addition. Theorem X.1.8 of
[Rosser] p. 276. (Contributed by SF,
16Jan2015.)

0_{c} 

Theorem  1cnnc 4408 
Cardinal one is a finite cardinal. Theorem X.1.12 of [Rosser] p. 277.
(Contributed by SF, 16Jan2015.)

1_{c} Nn 

Theorem  peano5 4409* 
The principle of mathematical induction: a set containing cardinal zero
and closed under the successor operator is a superset of the finite
cardinals. Theorem X.1.6 of [Rosser] p.
276. (Contributed by SF,
14Jan2015.)

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

Theorem  findsd 4410* 
Principle of finite induction over the finite cardinals, using implicit
substitutions. The first hypothesis ensures stratification of ,
the next four set up the substitutions, and the last two set up the base
case and induction hypothesis. This version allows for an extra
deduction clause that may make proving stratification simpler. Compare
Theorem X.1.13 of [Rosser] p. 277.
(Contributed by SF, 31Jul2019.)

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

Theorem  finds 4411* 
Principle of finite induction over the finite cardinals, using implicit
substitutions. The first hypothesis ensures stratification of ,
the next four set up the substitutions, and the last two set up the base
case and induction hypothesis. Compare Theorem X.1.13 of [Rosser]
p. 277. (Contributed by SF, 14Jan2015.)

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

Theorem  nnc0suc 4412* 
All naturals are either zero or a successor. Theorem X.1.7 of [Rosser]
p. 276. (Contributed by SF, 14Jan2015.)

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

Theorem  elsuc 4413* 
Membership in a successor. Theorem X.1.16 of [Rosser] p. 279.
(Contributed by SF, 16Jan2015.)

1_{c} ∼


Theorem  elsuci 4414 
Lemma for ncfinraise 4481. Take a natural and a disjoint union and
compute membership in the successor natural. (Contributed by SF,
22Jan2015.)

1_{c} 

Theorem  addcass 4415 
Cardinal addition is associative. Theorem X.1.11, corollary 1 of
[Rosser] p. 277. (Contributed by SF,
17Jan2015.)



Theorem  addc32 4416 
Swap arguments two and three in cardinal addition. (Contributed by SF,
22Jan2015.)



Theorem  addc4 4417 
Swap arguments two and three in quadruple cardinal addition. (Contributed
by SF, 25Jan2015.)



Theorem  addc6 4418 
Rearrange cardinal summation of six arguments. (Contributed by SF,
13Mar2015.)



Theorem  nncaddccl 4419 
The finite cardinals are closed under addition. Theorem X.1.14 of
[Rosser] p. 278. (Contributed by SF,
17Jan2015.)

Nn Nn Nn 

Theorem  elfin 4420* 
Membership in the set of finite sets. (Contributed by SF,
19Jan2015.)

Fin
Nn 

Theorem  el0c 4421 
Membership in cardinal zero. (Contributed by SF, 22Jan2015.)

0_{c}


Theorem  nulel0c 4422 
The empty set is a member of cardinal zero. (Contributed by SF,
13Feb2015.)

0_{c} 

Theorem  0fin 4423 
The empty set is finite. (Contributed by SF, 19Jan2015.)

Fin 

Theorem  nnsucelrlem1 4424* 
Lemma for nnsucelr 4428. Establish stratification for the inductive
hypothesis. (Contributed by SF, 15Jan2015.)

1_{c} 

Theorem  nnsucelrlem2 4425 
Lemma for nnsucelr 4428. Subtracting a nonelement from a set
adjoined
with the nonelement retrieves the original set. (Contributed by SF,
15Jan2015.)



Theorem  nnsucelrlem3 4426 
Lemma for nnsucelr 4428. Rearrange union and difference for a
particular
group of classes. (Contributed by SF, 15Jan2015.)



Theorem  nnsucelrlem4 4427 
Lemma for nnsucelr 4428. Remove and readjoin an element to a set.
(Contributed by SF, 15Jan2015.)



Theorem  nnsucelr 4428 
Transfer membership in the successor of a natural into membership of the
natural itself. Theorem X.1.17 of [Rosser] p. 525. (Contributed by SF,
14Jan2015.)

Nn
1_{c} 

Theorem  nndisjeq 4429 
Either two naturals are disjoint or they are the same natural. Theorem
X.1.18 of [Rosser] p. 526. (Contributed
by SF, 17Jan2015.)

Nn Nn 

Theorem  nnceleq 4430 
If two naturals have an element in common, then they are equal.
(Contributed by SF, 13Feb2015.)

Nn Nn


Theorem  snfi 4431 
A singleton is finite. (Contributed by SF, 23Feb2015.)

Fin 

2.2.11 Deriving infinity


Syntax  clefin 4432 
Extend class notation to include the less than or equal to relationship
for finite cardinals.

_{fin} 

Syntax  cltfin 4433 
Extend class notation to include the less than relationship for finite
cardinals.

_{fin} 

Syntax  cncfin 4434 
Extend class notation to include the finite cardinal function.

Nc_{fin} 

Syntax  ctfin 4435 
Extend class notation to include the finite T operation.

T_{fin} 

Syntax  cevenfin 4436 
Extend class notation to include the (temporary) set of all even
numbers.

Even_{fin} 

Syntax  coddfin 4437 
Extend class notation to include the (temporary) set of all odd
numbers.

Odd_{fin} 

Syntax  wsfin 4438 
Extend wff notation to include the finite S relationship.

S_{fin} 

Syntax  cspfin 4439 
Extend class notation to include the finite Sp set.

Sp_{fin} 

Definition  dflefin 4440* 
Define the less than or equal to relationship for finite cardinals.
Definition from Ex. X.1.4 of [Rosser] p.
279. (Contributed by SF,
12Jan2015.)

_{fin} Nn 

Definition  dfltfin 4441* 
Define the less than relationship for finite cardinals. Definition from
[Rosser] p. 527. (Contributed by SF,
12Jan2015.)

_{fin} Nn
1_{c} 

Definition  dfncfin 4442* 
Define the finite cardinal function. Definition from [Rosser] p. 527.
(Contributed by SF, 12Jan2015.)

Nc_{fin}
Nn 

Definition  dftfin 4443* 
Define the finite T operator. Definition from [Rosser] p. 528.
(Contributed by SF, 12Jan2015.)

T_{fin}
Nn _{1} 

Definition  dfevenfin 4444* 
Define the temporary set of all even numbers. This differs from the
final definition due to the nonnull condition. Definition from
[Rosser] p. 529. (Contributed by SF,
12Jan2015.)

Even_{fin}
Nn 

Definition  dfoddfin 4445* 
Define the temporary set of all odd numbers. This differs from the
final definition due to the nonnull condition. Definition from
[Rosser] p. 529. (Contributed by SF,
12Jan2015.)

Odd_{fin}
Nn 1_{c} 

Definition  dfsfin 4446* 
Define the finite S relationship. This relationship encapsulates the
idea of being
a "smaller" number than . Definition from
[Rosser] p. 530. (Contributed by SF,
12Jan2015.)

S_{fin} Nn Nn _{1} 

Definition  dfspfin 4447* 
Define the finite Sp set. Definition from [Rosser] p. 533.
(Contributed by SF, 12Jan2015.)

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


Theorem  opklefing 4448* 
Kuratowski ordered pair membership in finite less than or equal to.
(Contributed by SF, 18Jan2015.)

_{fin} Nn 

Theorem  opkltfing 4449* 
Kuratowski ordered pair membership in finite less than. (Contributed by
SF, 27Jan2015.)

_{fin} Nn 1_{c} 

Theorem  lefinaddc 4450 
Cardinal sum always yields a larger set. (Contributed by SF,
27Jan2015.)

Nn
_{fin} 

Theorem  prepeano4 4451 
Assuming a nonnull successor, cardinal successor is onetoone.
Theorem X.1.19 of [Rosser] p. 526.
(Contributed by SF, 18Jan2015.)

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

Theorem  addcnul1 4452 
Cardinal addition with the empty set. Theorem X.1.20, corollary 1 of
[Rosser] p. 526. (Contributed by SF,
18Jan2015.)



Theorem  addcnnul 4453 
If cardinal addition is nonempty, then both addends are nonempty.
Theorem X.1.20 of [Rosser] p. 526.
(Contributed by SF, 18Jan2015.)



Theorem  preaddccan2lem1 4454* 
Lemma for preaddccan2 4455. Establish stratification for the induction
step. (Contributed by SF, 30Mar2021.)

Nn Nn


Theorem  preaddccan2 4455 
Cancellation law for natural addition with a nonnull condition.
(Contributed by SF, 29Jan2015.)

Nn Nn Nn


Theorem  nulge 4456 
If the empty set is a finite cardinal, then it is a maximal element.
(Contributed by SF, 19Jan2015.)

Nn _{fin} 

Theorem  ltfinirr 4457 
Irreflexive law for finite less than. (Contributed by SF,
29Jan2015.)

Nn _{fin} 

Theorem  leltfintr 4458 
Transitivity law for finite less than and less than or equal.
(Contributed by SF, 2Feb2015.)

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

Theorem  ltfintr 4459 
Transitivity law for finite less than. (Contributed by SF,
29Jan2015.)

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

Theorem  ltfinasym 4460 
Asymmetry law for finite less than. (Contributed by SF, 29Jan2015.)

Nn Nn _{fin} _{fin} 

Theorem  0cminle 4461 
Cardinal zero is a minimal element for finite less than or equal.
(Contributed by SF, 29Jan2015.)

Nn 0_{c} _{fin} 

Theorem  ltfinp1 4462 
One plus a finite cardinal is strictly greater. (Contributed by SF,
29Jan2015.)

1_{c} _{fin} 

Theorem  lefinlteq 4463 
Transfer from less than or equal to less than. (Contributed by SF,
29Jan2015.)

_{fin} _{fin} 

Theorem  ltfinex 4464 
Finite less than is stratified. (Contributed by SF, 29Jan2015.)

_{fin} 

Theorem  ltfintrilem1 4465* 
Lemma for ltfintri 4466. Establish stratification for induction.
(Contributed by SF, 29Jan2015.)

Nn
_{fin} _{fin} 

Theorem  ltfintri 4466 
Trichotomy law for finite less than. (Contributed by SF,
29Jan2015.)

Nn Nn _{fin} _{fin} 

Theorem  lefinrflx 4467 
Less than or equal to is reflexive. (Contributed by SF, 2Feb2015.)

_{fin} 

Theorem  ltlefin 4468 
Less than implies less than or equal. (Contributed by SF,
2Feb2015.)

_{fin} _{fin} 

Theorem  lenltfin 4469 
Less than or equal is the same as negated less than. (Contributed by SF,
2Feb2015.)

Nn Nn _{fin} _{fin} 

Theorem  ssfin 4470 
A subset of a finite set is itself finite. Theorem X.1.21 of [Rosser]
p. 527. (Contributed by SF, 19Jan2015.)

Fin Fin 

Theorem  vfinnc 4471* 
If the universe is finite, then there is a unique natural containing any
set. Theorem X.1.22 of [Rosser] p. 527.
(Contributed by SF,
19Jan2015.)

Fin Nn 

Theorem  ncfinex 4472 
The finite cardinality of a set exists. (Contributed by SF,
27Jan2015.)

Nc_{fin}


Theorem  ncfineq 4473 
Equality theorem for finite cardinality. (Contributed by SF,
20Jan2015.)

Nc_{fin} Nc_{fin} 

Theorem  ncfinprop 4474 
Properties of finite cardinal number. Theorem X.1.23 of [Rosser] p. 527
(Contributed by SF, 20Jan2015.)

Fin Nc_{fin} Nn Nc_{fin} 

Theorem  ncfindi 4475 
Distribution law for finite cardinality. (Contributed by SF,
30Jan2015.)

Fin
Nc_{fin}
Nc_{fin} Nc_{fin} 

Theorem  ncfinsn 4476 
If the universe is finite, then the cardinality of a singleton is
1_{c}. (Contributed by SF, 30Jan2015.)

Fin Nc_{fin} 1_{c} 

Theorem  ncfineleq 4477 
Equality law for finite cardinality. Theorem X.1.24 of [Rosser]
p. 527. (Contributed by SF, 20Jan2015.)

Fin
Nc_{fin} Nc_{fin}
Nc_{fin} 

Theorem  eqpwrelk 4478 
Represent equality to power class via a Kuratowski relationship.
(Contributed by SF, 26Jan2015.)

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


Theorem  eqpw1relk 4479 
Represent equality to unit power class via a Kuratowski relationship.
(Contributed by SF, 21Jan2015.)

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

Theorem  ncfinraiselem2 4480* 
Lemma for ncfinraise 4481. Show stratification for induction.
(Contributed by SF, 22Jan2015.)

Nn _{1} _{1} 

Theorem  ncfinraise 4481* 
If two sets are in a particular finite cardinal, then their unit power
sets are in the same natural. Theorem X.1.25 of [Rosser] p. 527.
(Contributed by SF, 21Jan2015.)

Nn
Nn _{1} _{1} 

Theorem  ncfinlowerlem1 4482* 
Lemma for ncfinlower 4483. Set up stratification for induction.
(Contributed by SF, 22Jan2015.)

_{1} _{1}
Nn 

Theorem  ncfinlower 4483* 
If the unit power classes of two sets are in the same natural, then so
are the sets themselves. Theorem X.1.26 of [Rosser] p. 527.
(Contributed by SF, 22Jan2015.)

Nn _{1} _{1}
Nn 

Theorem  nnpw1ex 4484* 
For any nonempty finite cardinal, there is a unique natural containing
a unit power class of one of its elements. Theorem X.1.27 of [Rosser]
p. 528. (Contributed by SF, 22Jan2015.)

Nn
Nn _{1} 

Theorem  tfinex 4485 
The finite T operator is always a set. (Contributed by SF,
26Jan2015.)

T_{fin}


Theorem  eqtfinrelk 4486 
Equality to a T raising expressed via a Kuratowski relationship.
(Contributed by SF, 29Jan2015.)

_{k} ∼ Ins2_{k} S_{k} Ins3_{k} Ins3_{k} _{k}
S_{k} Ins2_{k} Ins2_{k} Nn _{k} Ins2_{k} SI_{k} S_{k} 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}_{k}_{1} _{1} _{1} 1_{c}
Ins3_{k} _{k} _{k}_{1} 1_{c}_{k}_{1} 1_{c}_{k}_{1} _{1} 1_{c} _{k} T_{fin} 

Theorem  tfinrelkex 4487 
The expression at the core of eqtfinrelk 4486 exists. (Contributed by SF,
30Jan2015.)

_{k} ∼ Ins2_{k} S_{k} Ins3_{k} Ins3_{k} _{k}
S_{k} Ins2_{k} Ins2_{k} Nn _{k} Ins2_{k} SI_{k} S_{k} 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}_{k}_{1} _{1} _{1} 1_{c}
Ins3_{k} _{k} _{k}_{1} 1_{c}_{k}_{1} 1_{c}_{k}_{1} _{1} 1_{c} _{k} 

Theorem  tfineq 4488 
Equality theorem for the finite T operator. (Contributed by SF,
24Jan2015.)

T_{fin} T_{fin} 

Theorem  tfinprop 4489* 
Properties of the finite T operator for a nonempty natural. Theorem
X.1.28 of [Rosser] p. 528. (Contributed
by SF, 22Jan2015.)

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

Theorem  tfinnnul 4490 
If is a nonempty
natural, then T_{fin} is also nonempty.
Corollary 1 of Theorem X.1.28 of [Rosser]
p. 528. (Contributed by SF,
23Jan2015.)

Nn
T_{fin} 

Theorem  tfinnul 4491 
The finite T operator applied to the empty set is empty. Theorem X.1.29
of [Rosser] p. 528. (Contributed by SF,
22Jan2015.)

T_{fin}


Theorem  tfincl 4492 
Closure law for finite T operation. (Contributed by SF, 2Feb2015.)

Nn T_{fin} Nn 

Theorem  tfin11 4493 
The finite T operator is onetoone over the naturals. Theorem X.1.30
of [Rosser] p. 528. (Contributed by SF,
24Jan2015.)

Nn Nn T_{fin}
T_{fin} 

Theorem  tfinpw1 4494 
The finite T operator on a natural contains the unit power class of any
element of the natural. Theorem X.1.31 of [Rosser] p. 528.
(Contributed by SF, 24Jan2015.)

Nn _{1} T_{fin} 

Theorem  ncfintfin 4495 
Relationship between finite T operator and finite Nc operation in a finite
universe. Corollary of Theorem X.1.31 of [Rosser] p. 529. (Contributed
by SF, 24Jan2015.)

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

Theorem  tfindi 4496 
The finite T operation distributes over nonempty cardinal sum. Theorem
X.1.32 of [Rosser] p. 529. (Contributed
by SF, 26Jan2015.)

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

Theorem  tfin0c 4497 
The finite T operator is fixed at 0_{c}. (Contributed by SF,
29Jan2015.)

T_{fin}
0_{c}
0_{c} 

Theorem  tfinsuc 4498 
The finite T operator over a successor. (Contributed by SF,
30Jan2015.)

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

Theorem  tfin1c 4499 
The finite T operator is idempotent over 1_{c}. Theorem
X.1.34(a) of
[Rosser] p. 529. (Contributed by SF,
30Jan2015.)

T_{fin}
1_{c}
1_{c} 

Theorem  tfinltfinlem1 4500 
Lemma for tfinltfin 4501. Prove the forward direction of the theorem.
(Contributed by SF, 2Feb2015.)

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