P. 73 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 7201-7300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oalimcl 7201	The ordinal sum with a limit ordinal is a limit ordinal. Proposition 8.11 of [TakeutiZaring] p. 60. (Contributed by NM, 8-Dec-2004.)
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> Lim ( A +o B ) )
Theorem	oaass 7202	Ordinal addition is associative. Theorem 25 of [Suppes] p. 211. (Contributed by NM, 10-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) )
Theorem	oarec 7203*	Recursive definition of ordinal addition. Exercise 25 of [Enderton] p. 240. (Contributed by NM, 26-Dec-2004.) (Revised by Mario Carneiro, 30-May-2015.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( A u. ran ( x e. B |-> ( A +o x ) ) ) )
Theorem	oaf1o 7204*	Left addition by a constant is a bijection from ordinals to ordinals greater than the constant. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( A e. On -> ( x e. On |-> ( A +o x ) ) : On -1-1-onto-> ( On \ A ) )
Theorem	oacomf1olem 7205*	Lemma for oacomf1o 7206. (Contributed by Mario Carneiro, 30-May-2015.)
|- F = ( x e. A |-> ( B +o x ) )   =>    |- ( ( A e. On /\ B e. On ) -> ( F : A -1-1-onto-> ran F /\ ( ran F i^i B ) = (/) ) )
Theorem	oacomf1o 7206*	Define a bijection from A +o B to B +o A. Thus, the two are equinumerous even if they are not equal (which sometimes occurs, e.g. oancom 8059). (Contributed by Mario Carneiro, 30-May-2015.)
|- F = ( ( x e. A |-> ( B +o x ) ) u. `' ( x e. B |-> ( A +o x ) ) )   =>    |- ( ( A e. On /\ B e. On ) -> F : ( A +o B ) -1-1-onto-> ( B +o A ) )
Theorem	omordi 7207	Ordering property of ordinal multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63. (Contributed by NM, 14-Dec-2004.)
|- ( ( ( B e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
Theorem	omord2 7208	Ordering property of ordinal multiplication. (Contributed by NM, 25-Dec-2004.)
|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A e. B <-> ( C .o A ) e. ( C .o B ) ) )
Theorem	omord 7209	Ordering property of ordinal multiplication. Proposition 8.19 of [TakeutiZaring] p. 63. (Contributed by NM, 14-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )
Theorem	omcan 7210	Left cancellation law for ordinal multiplication. Proposition 8.20 of [TakeutiZaring] p. 63 and its converse. (Contributed by NM, 14-Dec-2004.)
|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )
Theorem	omword 7211	Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004.)
|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )
Theorem	omwordi 7212	Weak ordering property of ordinal multiplication. (Contributed by NM, 21-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )
Theorem	omwordri 7213	Weak ordering property of ordinal multiplication. Proposition 8.21 of [TakeutiZaring] p. 63. (Contributed by NM, 20-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) )
Theorem	omword1 7214	An ordinal is less than or equal to its product with another. (Contributed by NM, 21-Dec-2004.)
|- ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> A C_ ( A .o B ) )
Theorem	omword2 7215	An ordinal is less than or equal to its product with another. (Contributed by NM, 21-Dec-2004.)
|- ( ( ( A e. On /\ B e. On ) /\ (/) e. B ) -> A C_ ( B .o A ) )
Theorem	om00 7216	The product of two ordinal numbers is zero iff at least one of them is zero. Proposition 8.22 of [TakeutiZaring] p. 64. (Contributed by NM, 21-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( ( A .o B ) = (/) <-> ( A = (/) \/ B = (/) ) ) )
Theorem	om00el 7217	The product of two nonzero ordinal numbers is nonzero. (Contributed by NM, 28-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( (/) e. ( A .o B ) <-> ( (/) e. A /\ (/) e. B ) ) )
Theorem	omordlim 7218*	Ordering involving the product of a limit ordinal. Proposition 8.23 of [TakeutiZaring] p. 64. (Contributed by NM, 25-Dec-2004.)
|- ( ( ( A e. On /\ ( B e. D /\ Lim B ) ) /\ C e. ( A .o B ) ) -> E. x e. B C e. ( A .o x ) )
Theorem	omlimcl 7219	The product of any nonzero ordinal with a limit ordinal is a limit ordinal. Proposition 8.24 of [TakeutiZaring] p. 64. (Contributed by NM, 25-Dec-2004.)
|- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> Lim ( A .o B ) )
Theorem	odi 7220	Distributive law for ordinal arithmetic (left-distributivity). Proposition 8.25 of [TakeutiZaring] p. 64. (Contributed by NM, 26-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
Theorem	omass 7221	Multiplication of ordinal numbers is associative. Theorem 8.26 of [TakeutiZaring] p. 65. (Contributed by NM, 28-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) )
Theorem	oneo 7222	If an ordinal number is even, its successor is odd. (Contributed by NM, 26-Jan-2006.)
|- ( ( A e. On /\ B e. On /\ C = ( 2o .o A ) ) -> -. suc C = ( 2o .o B ) )
Theorem	omeulem1 7223*	Lemma for omeu 7226: existence part. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E. x e. On E. y e. A ( ( A .o x ) +o y ) = B )
Theorem	omeulem2 7224	Lemma for omeu 7226: uniqueness part. (Contributed by Mario Carneiro, 28-Feb-2013.) (Revised by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( B e. D \/ ( B = D /\ C e. E ) ) -> ( ( A .o B ) +o C ) e. ( ( A .o D ) +o E ) ) )
Theorem	omopth2 7225	An ordered pair-like theorem for ordinal multiplication. (Contributed by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. On /\ A =/= (/) ) /\ ( B e. On /\ C e. A ) /\ ( D e. On /\ E e. A ) ) -> ( ( ( A .o B ) +o C ) = ( ( A .o D ) +o E ) <-> ( B = D /\ C = E ) ) )
Theorem	omeu 7226*	The division algorithm for ordinal multiplication. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- ( ( A e. On /\ B e. On /\ A =/= (/) ) -> E! z E. x e. On E. y e. A ( z = <. x , y >. /\ ( ( A .o x ) +o y ) = B ) )
Theorem	oen0 7227	Ordinal exponentiation with a nonzero mantissa is nonzero. Proposition 8.32 of [TakeutiZaring] p. 67. (Contributed by NM, 4-Jan-2005.)
|- ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> (/) e. ( A ^o B ) )
Theorem	oeordi 7228	Ordering law for ordinal exponentiation. Proposition 8.33 of [TakeutiZaring] p. 67. (Contributed by NM, 5-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( B e. On /\ C e. ( On \ 2o ) ) -> ( A e. B -> ( C ^o A ) e. ( C ^o B ) ) )
Theorem	oeord 7229	Ordering property of ordinal exponentiation. Corollary 8.34 of [TakeutiZaring] p. 68 and its converse. (Contributed by NM, 6-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A e. B <-> ( C ^o A ) e. ( C ^o B ) ) )
Theorem	oecan 7230	Left cancellation law for ordinal exponentiation. (Contributed by NM, 6-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( A e. ( On \ 2o ) /\ B e. On /\ C e. On ) -> ( ( A ^o B ) = ( A ^o C ) <-> B = C ) )
Theorem	oeword 7231	Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( A e. On /\ B e. On /\ C e. ( On \ 2o ) ) -> ( A C_ B <-> ( C ^o A ) C_ ( C ^o B ) ) )
Theorem	oewordi 7232	Weak ordering property of ordinal exponentiation. (Contributed by NM, 6-Jan-2005.)
|- ( ( ( A e. On /\ B e. On /\ C e. On ) /\ (/) e. C ) -> ( A C_ B -> ( C ^o A ) C_ ( C ^o B ) ) )
Theorem	oewordri 7233	Weak ordering property of ordinal exponentiation. Proposition 8.35 of [TakeutiZaring] p. 68. (Contributed by NM, 6-Jan-2005.)
|- ( ( B e. On /\ C e. On ) -> ( A e. B -> ( A ^o C ) C_ ( B ^o C ) ) )
Theorem	oeworde 7234	Ordinal exponentiation compared to its exponent. Proposition 8.37 of [TakeutiZaring] p. 68. (Contributed by NM, 7-Jan-2005.) (Revised by Mario Carneiro, 24-May-2015.)
|- ( ( A e. ( On \ 2o ) /\ B e. On ) -> B C_ ( A ^o B ) )
Theorem	oeordsuc 7235	Ordering property of ordinal exponentiation with a successor exponent. Corollary 8.36 of [TakeutiZaring] p. 68. (Contributed by NM, 7-Jan-2005.)
|- ( ( B e. On /\ C e. On ) -> ( A e. B -> ( A ^o suc C ) e. ( B ^o suc C ) ) )
Theorem	oelim2 7236*	Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of [Mendelson] p. 250. (Contributed by NM, 6-Jan-2005.)
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A ^o B ) = U_ x e. ( B \ 1o ) ( A ^o x ) )
Theorem	oeoalem 7237	Lemma for oeoa 7238. (Contributed by Eric Schmidt, 26-May-2009.)
|- A e. On   &    |- (/) e. A   &    |- B e. On   =>    |- ( C e. On -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )
Theorem	oeoa 7238	Sum of exponents law for ordinal exponentiation. Theorem 8R of [Enderton] p. 238. Also Proposition 8.41 of [TakeutiZaring] p. 69. (Contributed by Eric Schmidt, 26-May-2009.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A ^o ( B +o C ) ) = ( ( A ^o B ) .o ( A ^o C ) ) )
Theorem	oeoelem 7239	Lemma for oeoe 7240. (Contributed by Eric Schmidt, 26-May-2009.)
|- A e. On   &    |- (/) e. A   =>    |- ( ( B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )
Theorem	oeoe 7240	Product of exponents law for ordinal exponentiation. Theorem 8S of [Enderton] p. 238. Also Proposition 8.42 of [TakeutiZaring] p. 70. (Contributed by Eric Schmidt, 26-May-2009.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A ^o B ) ^o C ) = ( A ^o ( B .o C ) ) )
Theorem	oelimcl 7241	The ordinal exponential with a limit ordinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2015.)
|- ( ( A e. ( On \ 2o ) /\ ( B e. C /\ Lim B ) ) -> Lim ( A ^o B ) )
Theorem	oeeulem 7242*	Lemma for oeeu 7244. (Contributed by Mario Carneiro, 28-Feb-2013.)
|- X = U. |^| { x e. On | B e. ( A ^o x ) }   =>    |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( X e. On /\ ( A ^o X ) C_ B /\ B e. ( A ^o suc X ) ) )
Theorem	oeeui 7243*	The division algorithm for ordinal exponentiation. (This version of oeeu 7244 gives an explicit expression for the unique solution of the equation, in terms of the solution P to omeu 7226.) (Contributed by Mario Carneiro, 25-May-2015.)
|- X = U. |^| { x e. On | B e. ( A ^o x ) }   &    |- P = ( iota w E. y e. On E. z e. ( A ^o X ) ( w = <. y , z >. /\ ( ( ( A ^o X ) .o y ) +o z ) = B ) )   &    |- Y = ( 1st ` P )   &    |- Z = ( 2nd ` P )   =>    |- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> ( ( ( C e. On /\ D e. ( A \ 1o ) /\ E e. ( A ^o C ) ) /\ ( ( ( A ^o C ) .o D ) +o E ) = B ) <-> ( C = X /\ D = Y /\ E = Z ) ) )
Theorem	oeeu 7244*	The division algorithm for ordinal exponentiation. (Contributed by Mario Carneiro, 25-May-2015.)
|- ( ( A e. ( On \ 2o ) /\ B e. ( On \ 1o ) ) -> E! w E. x e. On E. y e. ( A \ 1o ) E. z e. ( A ^o x ) ( w = <. x , y , z >. /\ ( ( ( A ^o x ) .o y ) +o z ) = B ) )
2.4.18  Natural number arithmetic
Theorem	nna0 7245	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A +o (/) ) = A )
Theorem	nnm0 7246	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.)
|- ( A e. om -> ( A .o (/) ) = (/) )
Theorem	nnasuc 7247	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	nnmsuc 7248	Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
Theorem	nnesuc 7249	Exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
Theorem	nna0r 7250	Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81. Note: In this and later theorems, we deliberately avoid the more general ordinal versions of these theorems (in this case oa0r 7180) so that we can avoid ax-rep 4553, which is not needed for finite recursive definitions. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- ( A e. om -> ( (/) +o A ) = A )
Theorem	nnm0r 7251	Multiplication with zero. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( A e. om -> ( (/) .o A ) = (/) )
Theorem	nnacl 7252	Closure of addition of natural numbers. Proposition 8.9 of [TakeutiZaring] p. 59. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A +o B ) e. om )
Theorem	nnmcl 7253	Closure of multiplication of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63. (Contributed by NM, 20-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A .o B ) e. om )
Theorem	nnecl 7254	Closure of exponentiation of natural numbers. Proposition 8.17 of [TakeutiZaring] p. 63. (Contributed by NM, 24-Mar-2007.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A ^o B ) e. om )
Theorem	nnacli 7255	om is closed under addition. Inference form of nnacl 7252. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A +o B ) e. om
Theorem	nnmcli 7256	om is closed under multiplication. Inference form of nnmcl 7253. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &    |- B e. om   =>    |- ( A .o B ) e. om
Theorem	nnarcl 7257	Reverse closure law for addition of natural numbers. Exercise 1 of [TakeutiZaring] p. 62 and its converse. (Contributed by NM, 12-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) e. om <-> ( A e. om /\ B e. om ) ) )
Theorem	nnacom 7258	Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 6-May-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A +o B ) = ( B +o A ) )
Theorem	nnaordi 7259	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers. (Contributed by NM, 3-Feb-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( B e. om /\ C e. om ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaord 7260	Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58, limited to natural numbers, and its converse. (Contributed by NM, 7-Mar-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
Theorem	nnaordr 7261	Ordering property of addition of natural numbers. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A e. B <-> ( A +o C ) e. ( B +o C ) ) )
Theorem	nnawordi 7262	Adding to both sides of an inequality in om (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) )
Theorem	nnaass 7263	Addition of natural numbers is associative. Theorem 4K(1) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) )
Theorem	nndi 7264	Distributive law for natural numbers (left-distributivity). Theorem 4K(3) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A .o ( B +o C ) ) = ( ( A .o B ) +o ( A .o C ) ) )
Theorem	nnmass 7265	Multiplication of natural numbers is associative. Theorem 4K(4) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A .o B ) .o C ) = ( A .o ( B .o C ) ) )
Theorem	nnmsucr 7266	Multiplication with successor. Exercise 16 of [Enderton] p. 82. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( suc A .o B ) = ( ( A .o B ) +o B ) )
Theorem	nnmcom 7267	Multiplication of natural numbers is commutative. Theorem 4K(5) of [Enderton] p. 81. (Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. om /\ B e. om ) -> ( A .o B ) = ( B .o A ) )
Theorem	nnaword 7268	Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B <-> ( C +o A ) C_ ( C +o B ) ) )
Theorem	nnacan 7269	Cancellation law for addition of natural numbers. (Contributed by NM, 27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )
Theorem	nnaword1 7270	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( A +o B ) )
Theorem	nnaword2 7271	Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|- ( ( A e. om /\ B e. om ) -> A C_ ( B +o A ) )
Theorem	nnmordi 7272	Ordering property of multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by NM, 18-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( ( B e. om /\ C e. om ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmord 7273	Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by NM, 22-Jan-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( ( A e. B /\ (/) e. C ) <-> ( C .o A ) e. ( C .o B ) ) )
Theorem	nnmword 7274	Weak ordering property of ordinal multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. C ) -> ( A C_ B <-> ( C .o A ) C_ ( C .o B ) ) )
Theorem	nnmcan 7275	Cancellation law for multiplication of natural numbers. (Contributed by NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( ( A e. om /\ B e. om /\ C e. om ) /\ (/) e. A ) -> ( ( A .o B ) = ( A .o C ) <-> B = C ) )
Theorem	nnmwordi 7276	Weak ordering property of multiplication. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( C .o A ) C_ ( C .o B ) ) )
Theorem	nnmwordri 7277	Weak ordering property of ordinal multiplication. Proposition 8.21 of [TakeutiZaring] p. 63, limited to natural numbers. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C e. om ) -> ( A C_ B -> ( A .o C ) C_ ( B .o C ) ) )
Theorem	nnawordex 7278*	Equivalence for weak ordering of natural numbers. (Contributed by NM, 8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A C_ B <-> E. x e. om ( A +o x ) = B ) )
Theorem	nnaordex 7279*	Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88. (Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( ( A e. om /\ B e. om ) -> ( A e. B <-> E. x e. om ( (/) e. x /\ ( A +o x ) = B ) ) )
Theorem	1onn 7280	One is a natural number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. om
Theorem	2onn 7281	The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|- 2o e. om
Theorem	3onn 7282	The ordinal 3 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. om
Theorem	4onn 7283	The ordinal 4 is a natural number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. om
Theorem	oaabslem 7284	Lemma for oaabs 7285. (Contributed by NM, 9-Dec-2004.)
|- ( ( om e. On /\ A e. om ) -> ( A +o om ) = om )
Theorem	oaabs 7285	Ordinal addition absorbs a natural number added to the left of a transfinite number. Proposition 8.10 of [TakeutiZaring] p. 59. (Contributed by NM, 9-Dec-2004.) (Proof shortened by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. om /\ B e. On ) /\ om C_ B ) -> ( A +o B ) = B )
Theorem	oaabs2 7286	The absorption law oaabs 7285 is also a property of higher powers of om. (Contributed by Mario Carneiro, 29-May-2015.)
|- ( ( ( A e. ( om ^o C ) /\ B e. On ) /\ ( om ^o C ) C_ B ) -> ( A +o B ) = B )
Theorem	omabslem 7287	Lemma for omabs 7288. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( ( om e. On /\ A e. om /\ (/) e. A ) -> ( A .o om ) = om )
Theorem	omabs 7288	Ordinal multiplication is also absorbed by powers of om. (Contributed by Mario Carneiro, 30-May-2015.)
|- ( ( ( A e. om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) -> ( A .o ( om ^o B ) ) = ( om ^o B ) )
Theorem	nnm1 7289	Multiply an element of om by 1o. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 1o ) = A )
Theorem	nnm2 7290	Multiply an element of om by 2o (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( A .o 2o ) = ( A +o A ) )
Theorem	nn2m 7291	Multiply an element of om by 2o (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- ( A e. om -> ( 2o .o A ) = ( A +o A ) )
Theorem	nnneo 7292	If a natural number is even, its successor is odd. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. om /\ B e. om /\ C = ( 2o .o A ) ) -> -. suc C = ( 2o .o B ) )
Theorem	nneob 7293*	A natural number is even iff its successor is odd. (Contributed by NM, 26-Jan-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- ( A e. om -> ( E. x e. om A = ( 2o .o x ) <-> -. E. x e. om suc A = ( 2o .o x ) ) )
Theorem	omsmolem 7294*	Lemma for omsmo 7295. (Contributed by NM, 30-Nov-2003.) (Revised by David Abernethy, 1-Jan-2014.)
|- ( y e. om -> ( ( ( A C_ On /\ F : om --> A ) /\ A. x e. om ( F ` x ) e. ( F ` suc x ) ) -> ( z e. y -> ( F ` z ) e. ( F ` y ) ) ) )
Theorem	omsmo 7295*	A strictly monotonic ordinal function on the set of natural numbers is one-to-one. (Contributed by NM, 30-Nov-2003.) (Revised by David Abernethy, 1-Jan-2014.)
|- ( ( ( A C_ On /\ F : om --> A ) /\ A. x e. om ( F ` x ) e. ( F ` suc x ) ) -> F : om -1-1-> A )
Theorem	omopthlem1 7296	Lemma for omopthi 7298. (Contributed by Scott Fenton, 18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- A e. om   &    |- C e. om   =>    |- ( A e. C -> ( ( A .o A ) +o ( A .o 2o ) ) e. ( C .o C ) )
Theorem	omopthlem2 7297	Lemma for omopthi 7298. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- A e. om   &    |- B e. om   &    |- C e. om   &    |- D e. om   =>    |- ( ( A +o B ) e. C -> -. ( ( C .o C ) +o D ) = ( ( ( A +o B ) .o ( A +o B ) ) +o B ) )
Theorem	omopthi 7298	An ordered pair theorem for om. Theorem 17.3 of [Quine] p. 124. This proof is adapted from nn0opthi 12307. (Contributed by Scott Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- A e. om   &    |- B e. om   &    |- C e. om   &    |- D e. om   =>    |- ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( A = C /\ B = D ) )
Theorem	omopth 7299	An ordered pair theorem for finite integers. Analogous to nn0opthi 12307. (Contributed by Scott Fenton, 1-May-2012.)
|- ( ( ( A e. om /\ B e. om ) /\ ( C e. om /\ D e. om ) ) -> ( ( ( ( A +o B ) .o ( A +o B ) ) +o B ) = ( ( ( C +o D ) .o ( C +o D ) ) +o D ) <-> ( A = C /\ B = D ) ) )
2.4.19  Equivalence relations and classes
Syntax	wer 7300	Extend the definition of a wff to include the equivalence predicate.
wff R Er A