Type  Label  Description 
Statement 

Theorem  oa0 6401 
Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57.
(Contributed by NM, 3May1995.) (Revised by Mario Carneiro,
8Sep2013.)



Theorem  om0 6402 
Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring]
p. 62. (Contributed by NM, 17Sep1995.) (Revised by Mario Carneiro,
8Sep2013.)



Theorem  oei0 6403 
Ordinal exponentiation with zero exponent. Definition 8.30 of
[TakeutiZaring] p. 67.
(Contributed by NM, 31Dec2004.) (Revised by
Mario Carneiro, 8Sep2013.)

↑_{o} 

Theorem  oacl 6404 
Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring]
p. 57. (Contributed by NM, 5May1995.) (Constructive proof by Jim
Kingdon, 26Jul2019.)



Theorem  omcl 6405 
Closure law for ordinal multiplication. Proposition 8.16 of
[TakeutiZaring] p. 57.
(Contributed by NM, 3Aug2004.) (Constructive
proof by Jim Kingdon, 26Jul2019.)



Theorem  oeicl 6406 
Closure law for ordinal exponentiation. (Contributed by Jim Kingdon,
26Jul2019.)

↑_{o} 

Theorem  oav2 6407* 
Value of ordinal addition. (Contributed by Mario Carneiro and Jim
Kingdon, 12Aug2019.)



Theorem  oasuc 6408 
Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56.
(Contributed by NM, 3May1995.) (Revised by Mario Carneiro,
8Sep2013.)



Theorem  omv2 6409* 
Value of ordinal multiplication. (Contributed by Jim Kingdon,
23Aug2019.)



Theorem  onasuc 6410 
Addition with successor. Theorem 4I(A2) of [Enderton] p. 79.
(Contributed by Mario Carneiro, 16Nov2014.)



Theorem  oa1suc 6411 
Addition with 1 is same as successor. Proposition 4.34(a) of [Mendelson]
p. 266. (Contributed by NM, 29Oct1995.) (Revised by Mario Carneiro,
16Nov2014.)



Theorem  o1p1e2 6412 
1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18Feb2004.)



Theorem  oawordi 6413 
Weak ordering property of ordinal addition. (Contributed by Jim
Kingdon, 27Jul2019.)



Theorem  oawordriexmid 6414* 
A weak ordering property of ordinal addition which implies excluded
middle. The property is proposition 8.7 of [TakeutiZaring] p. 59.
Compare with oawordi 6413. (Contributed by Jim Kingdon, 15May2022.)



Theorem  oaword1 6415 
An ordinal is less than or equal to its sum with another. Part of
Exercise 5 of [TakeutiZaring] p. 62.
(Contributed by NM, 6Dec2004.)



Theorem  omsuc 6416 
Multiplication with successor. Definition 8.15 of [TakeutiZaring]
p. 62. (Contributed by NM, 17Sep1995.) (Revised by Mario Carneiro,
8Sep2013.)



Theorem  onmsuc 6417 
Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80.
(Contributed by NM, 20Sep1995.) (Revised by Mario Carneiro,
14Nov2014.)



2.6.24 Natural number arithmetic


Theorem  nna0 6418 
Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by
NM, 20Sep1995.)



Theorem  nnm0 6419 
Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80.
(Contributed by NM, 20Sep1995.)



Theorem  nnasuc 6420 
Addition with successor. Theorem 4I(A2) of [Enderton] p. 79.
(Contributed by NM, 20Sep1995.) (Revised by Mario Carneiro,
14Nov2014.)



Theorem  nnmsuc 6421 
Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80.
(Contributed by NM, 20Sep1995.) (Revised by Mario Carneiro,
14Nov2014.)



Theorem  nna0r 6422 
Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81.
(Contributed by NM, 20Sep1995.) (Revised by Mario Carneiro,
14Nov2014.)



Theorem  nnm0r 6423 
Multiplication with zero. Exercise 16 of [Enderton] p. 82.
(Contributed by NM, 20Sep1995.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  nnacl 6424 
Closure of addition of natural numbers. Proposition 8.9 of
[TakeutiZaring] p. 59.
(Contributed by NM, 20Sep1995.) (Proof
shortened by Andrew Salmon, 22Oct2011.)



Theorem  nnmcl 6425 
Closure of multiplication of natural numbers. Proposition 8.17 of
[TakeutiZaring] p. 63.
(Contributed by NM, 20Sep1995.) (Proof
shortened by Andrew Salmon, 22Oct2011.)



Theorem  nnacli 6426 
is closed under
addition. Inference form of nnacl 6424.
(Contributed by Scott Fenton, 20Apr2012.)



Theorem  nnmcli 6427 
is closed under
multiplication. Inference form of nnmcl 6425.
(Contributed by Scott Fenton, 20Apr2012.)



Theorem  nnacom 6428 
Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton]
p. 81. (Contributed by NM, 6May1995.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  nnaass 6429 
Addition of natural numbers is associative. Theorem 4K(1) of [Enderton]
p. 81. (Contributed by NM, 20Sep1995.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  nndi 6430 
Distributive law for natural numbers (leftdistributivity). Theorem
4K(3) of [Enderton] p. 81.
(Contributed by NM, 20Sep1995.) (Revised
by Mario Carneiro, 15Nov2014.)



Theorem  nnmass 6431 
Multiplication of natural numbers is associative. Theorem 4K(4) of
[Enderton] p. 81. (Contributed by NM,
20Sep1995.) (Revised by Mario
Carneiro, 15Nov2014.)



Theorem  nnmsucr 6432 
Multiplication with successor. Exercise 16 of [Enderton] p. 82.
(Contributed by NM, 21Sep1995.) (Proof shortened by Andrew Salmon,
22Oct2011.)



Theorem  nnmcom 6433 
Multiplication of natural numbers is commutative. Theorem 4K(5) of
[Enderton] p. 81. (Contributed by NM,
21Sep1995.) (Proof shortened
by Andrew Salmon, 22Oct2011.)



Theorem  nndir 6434 
Distributive law for natural numbers (rightdistributivity). (Contributed
by Jim Kingdon, 3Dec2019.)



Theorem  nnsucelsuc 6435 
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucelsucr 4466, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucelsucexmid 4488.
(Contributed by Jim Kingdon, 25Aug2019.)



Theorem  nnsucsssuc 6436 
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucsssucr 4467, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucsssucexmid 4485.
(Contributed by Jim Kingdon, 25Aug2019.)



Theorem  nntri3or 6437 
Trichotomy for natural numbers. (Contributed by Jim Kingdon,
25Aug2019.)



Theorem  nntri2 6438 
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28Aug2019.)



Theorem  nnsucuniel 6439 
Given an element of
the union of a natural number ,
is an element of itself. The reverse
direction holds
for all ordinals (sucunielr 4468). The forward direction for all
ordinals implies excluded middle (ordsucunielexmid 4489). (Contributed
by Jim Kingdon, 13Mar2022.)



Theorem  nntri1 6440 
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28Aug2019.)



Theorem  nntri3 6441 
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15May2020.)



Theorem  nntri2or2 6442 
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15Sep2021.)



Theorem  nndceq 6443 
Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p.
(varies). For the specific case where is zero, see nndceq0 4576.
(Contributed by Jim Kingdon, 31Aug2019.)

DECID


Theorem  nndcel 6444 
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6Sep2019.)

DECID


Theorem  nnsseleq 6445 
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16Sep2021.)



Theorem  nnsssuc 6446 
A natural number is a subset of another natural number if and only if it
belongs to its successor. (Contributed by Jim Kingdon, 22Jul2023.)



Theorem  nntr2 6447 
Transitive law for natural numbers. (Contributed by Jim Kingdon,
22Jul2023.)



Theorem  dcdifsnid 6448* 
If we remove a single element from a set with decidable equality then
put it back in, we end up with the original set. This strengthens
difsnss 3702 from subset to equality but the proof relies
on equality being
decidable. (Contributed by Jim Kingdon, 17Jun2022.)

DECID


Theorem  fnsnsplitdc 6449* 
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27Feb2015.) (Revised by Jim Kingdon, 29Jan2023.)

DECID 

Theorem  funresdfunsndc 6450* 
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value
of the element results in the function itself, where equality is
decidable. (Contributed by AV, 2Dec2018.) (Revised by Jim Kingdon,
30Jan2023.)

DECID


Theorem  nndifsnid 6451 
If we remove a single element from a natural number then put it back in,
we end up with the original natural number. This strengthens difsnss 3702
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31Aug2021.)



Theorem  nnaordi 6452 
Ordering property of addition. Proposition 8.4 of [TakeutiZaring]
p. 58, limited to natural numbers. (Contributed by NM, 3Feb1996.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaord 6453 
Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58,
limited to natural numbers, and its converse. (Contributed by NM,
7Mar1996.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaordr 6454 
Ordering property of addition of natural numbers. (Contributed by NM,
9Nov2002.)



Theorem  nnaword 6455 
Weak ordering property of addition. (Contributed by NM, 17Sep1995.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnacan 6456 
Cancellation law for addition of natural numbers. (Contributed by NM,
27Oct1995.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaword1 6457 
Weak ordering property of addition. (Contributed by NM, 9Nov2002.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnaword2 6458 
Weak ordering property of addition. (Contributed by NM, 9Nov2002.)



Theorem  nnawordi 6459 
Adding to both sides of an inequality in (Contributed by Scott
Fenton, 16Apr2012.) (Revised by Mario Carneiro, 12May2012.)



Theorem  nnmordi 6460 
Ordering property of multiplication. Half of Proposition 8.19 of
[TakeutiZaring] p. 63, limited to
natural numbers. (Contributed by NM,
18Sep1995.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnmord 6461 
Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring]
p. 63, limited to natural numbers. (Contributed by NM, 22Jan1996.)
(Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnmword 6462 
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17Nov2014.)



Theorem  nnmcan 6463 
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26Oct1995.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  1onn 6464 
One is a natural number. (Contributed by NM, 29Oct1995.)



Theorem  2onn 6465 
The ordinal 2 is a natural number. (Contributed by NM, 28Sep2004.)



Theorem  3onn 6466 
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5Jan2016.)



Theorem  4onn 6467 
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5Jan2016.)



Theorem  nnm1 6468 
Multiply an element of by .
(Contributed by Mario
Carneiro, 17Nov2014.)



Theorem  nnm2 6469 
Multiply an element of by .
(Contributed by Scott Fenton,
18Apr2012.) (Revised by Mario Carneiro, 17Nov2014.)



Theorem  nn2m 6470 
Multiply an element of by .
(Contributed by Scott Fenton,
16Apr2012.) (Revised by Mario Carneiro, 17Nov2014.)



Theorem  nnaordex 6471* 
Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
(Contributed by NM, 5Dec1995.) (Revised by Mario Carneiro,
15Nov2014.)



Theorem  nnawordex 6472* 
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8Nov2002.) (Revised by Mario Carneiro, 15Nov2014.)



Theorem  nnm00 6473 
The product of two natural numbers is zero iff at least one of them is
zero. (Contributed by Jim Kingdon, 11Nov2004.)



2.6.25 Equivalence relations and
classes


Syntax  wer 6474 
Extend the definition of a wff to include the equivalence predicate.



Syntax  cec 6475 
Extend the definition of a class to include equivalence class.



Syntax  cqs 6476 
Extend the definition of a class to include quotient set.



Definition  dfer 6477 
Define the equivalence relation predicate. Our notation is not standard.
A formal notation doesn't seem to exist in the literature; instead only
informal English tends to be used. The present definition, although
somewhat cryptic, nicely avoids dummy variables. In dfer2 6478 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6497, ersymb 6491, and ertr 6492.
(Contributed by NM, 4Jun1995.) (Revised by Mario Carneiro,
2Nov2015.)



Theorem  dfer2 6478* 
Alternate definition of equivalence predicate. (Contributed by NM,
3Jan1997.) (Revised by Mario Carneiro, 12Aug2015.)



Definition  dfec 6479 
Define the coset of
. Exercise 35 of [Enderton] p. 61. This
is called the equivalence class of modulo when is an
equivalence relation (i.e. when ; see dfer2 6478). In this case,
is a
representative (member) of the equivalence class ,
which contains all sets that are equivalent to . Definition of
[Enderton] p. 57 uses the notation (subscript) , although
we simply follow the brackets by since we don't have subscripted
expressions. For an alternate definition, see dfec2 6480. (Contributed by
NM, 23Jul1995.)



Theorem  dfec2 6480* 
Alternate definition of coset of .
Definition 34 of
[Suppes] p. 81. (Contributed by NM,
3Jan1997.) (Proof shortened by
Mario Carneiro, 9Jul2014.)



Theorem  ecexg 6481 
An equivalence class modulo a set is a set. (Contributed by NM,
24Jul1995.)



Theorem  ecexr 6482 
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9Jul2014.)



Definition  dfqs 6483* 
Define quotient set.
is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23Jul1995.)



Theorem  ereq1 6484 
Equality theorem for equivalence predicate. (Contributed by NM,
4Jun1995.) (Revised by Mario Carneiro, 12Aug2015.)



Theorem  ereq2 6485 
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12Aug2015.)



Theorem  errel 6486 
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12Aug2015.)



Theorem  erdm 6487 
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12Aug2015.)



Theorem  ercl 6488 
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12Aug2015.)



Theorem  ersym 6489 
An equivalence relation is symmetric. (Contributed by NM, 4Jun1995.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ercl2 6490 
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12Aug2015.)



Theorem  ersymb 6491 
An equivalence relation is symmetric. (Contributed by NM, 30Jul1995.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ertr 6492 
An equivalence relation is transitive. (Contributed by NM, 4Jun1995.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ertrd 6493 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ertr2d 6494 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ertr3d 6495 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  ertr4d 6496 
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9Jul2014.)



Theorem  erref 6497 
An equivalence relation is reflexive on its field. Compare Theorem 3M
of [Enderton] p. 56. (Contributed by
Mario Carneiro, 6May2013.)
(Revised by Mario Carneiro, 12Aug2015.)



Theorem  ercnv 6498 
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12Aug2015.)



Theorem  errn 6499 
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11Oct2010.) (Revised by Mario Carneiro,
12Aug2015.)



Theorem  erssxp 6500 
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12Aug2015.)

