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	2on 7201	Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
|- 2o e. On
Theorem	2on0 7202	Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.)
|- 2o =/= (/)
Theorem	3on 7203	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. On
Theorem	4on 7204	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. On
Theorem	df1o2 7205	Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
|- 1o = { (/) }
Theorem	df2o3 7206	Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- 2o = { (/) , 1o }
Theorem	df2o2 7207	Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.)
|- 2o = { (/) , { (/) } }
Theorem	1n0 7208	Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)
|- 1o =/= (/)
Theorem	xp01disj 7209	Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by NM, 2-Jun-2007.)
|- ( ( A X. { (/) } ) i^i ( C X. { 1o } ) ) = (/)
Theorem	ordgt0ge1 7210	Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.)
|- ( Ord A -> ( (/) e. A <-> 1o C_ A ) )
Theorem	ordge1n0 7211	An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004.)
|- ( Ord A -> ( 1o C_ A <-> A =/= (/) ) )
Theorem	el1o 7212	Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)
|- ( A e. 1o <-> A = (/) )
Theorem	dif1o 7213	Two ways to say that A is a nonzero number of the set B. (Contributed by Mario Carneiro, 21-May-2015.)
|- ( A e. ( B \ 1o ) <-> ( A e. B /\ A =/= (/) ) )
Theorem	ondif1 7214	Two ways to say that A is a nonzero ordinal number. (Contributed by Mario Carneiro, 21-May-2015.)
|- ( A e. ( On \ 1o ) <-> ( A e. On /\ (/) e. A ) )
Theorem	ondif2 7215	Two ways to say that A is an ordinal greater than one. (Contributed by Mario Carneiro, 21-May-2015.)
|- ( A e. ( On \ 2o ) <-> ( A e. On /\ 1o e. A ) )
Theorem	2oconcl 7216	Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( A e. 2o -> ( 1o \ A ) e. 2o )
Theorem	0lt1o 7217	Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)
|- (/) e. 1o
Theorem	dif20el 7218	An ordinal greater than one is greater than zero. (Contributed by Mario Carneiro, 25-May-2015.)
|- ( A e. ( On \ 2o ) -> (/) e. A )
Theorem	0we1 7219	The empty set is a well-ordering of ordinal one. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- (/) We 1o
Theorem	brwitnlem 7220	Lemma for relations which assert the existence of a witness in a two-parameter set. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 23-Aug-2015.)
|- R = ( `' O " ( _V \ 1o ) )   &    |- O Fn X   =>    |- ( A R B <-> ( A O B ) =/= (/) )
Theorem	fnoa 7221	Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- +o Fn ( On X. On )
Theorem	fnom 7222	Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- .o Fn ( On X. On )
Theorem	fnoe 7223	Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.)
|- ^o Fn ( On X. On )
Theorem	oav 7224*	Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( rec ( ( x e. _V |-> suc x ) , A ) ` B ) )
Theorem	omv 7225*	Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) = ( rec ( ( x e. _V |-> ( x +o A ) ) , (/) ) ` B ) )
Theorem	oe0lem 7226	A helper lemma for oe0 7235 and others. (Contributed by NM, 6-Jan-2005.)
|- ( ( ph /\ A = (/) ) -> ps )   &    |- ( ( ( A e. On /\ ph ) /\ (/) e. A ) -> ps )   =>    |- ( ( A e. On /\ ph ) -> ps )
Theorem	oev 7227*	Value of ordinal exponentiation. (Contributed by NM, 30-Dec-2004.) (Revised by Mario Carneiro, 23-Aug-2014.)
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) = if ( A = (/) , ( 1o \ B ) , ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )
Theorem	oevn0 7228*	Value of ordinal exponentiation at a nonzero mantissa. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( ( A e. On /\ B e. On ) /\ (/) e. A ) -> ( A ^o B ) = ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) )
Theorem	oa0 7229	Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( A +o (/) ) = A )
Theorem	om0 7230	Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( A .o (/) ) = (/) )
Theorem	oe0m 7231	Ordinal exponentiation with zero mantissa. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( (/) ^o A ) = ( 1o \ A ) )
Theorem	om0x 7232	Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. Unlike om0 7230, this version works whether or not A is an ordinal. However, since it is an artifact of our particular function value definition outside the domain, we will not use it in order to be conventional and present it only as a curiosity. (Contributed by NM, 1-Feb-1996.)
|- ( A .o (/) ) = (/)
Theorem	oe0m0 7233	Ordinal exponentiation with zero mantissa and zero exponent. Proposition 8.31 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.)
|- ( (/) ^o (/) ) = 1o
Theorem	oe0m1 7234	Ordinal exponentiation with zero mantissa and nonzero exponent. Proposition 8.31(2) of [TakeutiZaring] p. 67 and its converse. (Contributed by NM, 5-Jan-2005.)
|- ( A e. On -> ( (/) e. A <-> ( (/) ^o A ) = (/) ) )
Theorem	oe0 7235	Ordinal exponentiation with zero exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( A e. On -> ( A ^o (/) ) = 1o )
Theorem	oev2 7236*	Alternate value of ordinal exponentiation. Compare oev 7227. (Contributed by NM, 2-Jan-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) = ( ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) i^i ( ( _V \ |^| A ) u. |^| B ) ) )
Theorem	oasuc 7237	Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	oesuclem 7238*	Lemma for oesuc 7240. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
|- Lim X   &    |- ( B e. X -> ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` suc B ) = ( ( x e. _V |-> ( x .o A ) ) ` ( rec ( ( x e. _V |-> ( x .o A ) ) , 1o ) ` B ) ) )   =>    |- ( ( A e. On /\ B e. X ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
Theorem	omsuc 7239	Multiplication with successor. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
Theorem	oesuc 7240	Ordinal exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ B e. On ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
Theorem	onasuc 7241	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Note that this version of oasuc 7237 does not need Replacement.) (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ( ( A e. On /\ B e. om ) -> ( A +o suc B ) = suc ( A +o B ) )
Theorem	onmsuc 7242	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. On /\ B e. om ) -> ( A .o suc B ) = ( ( A .o B ) +o A ) )
Theorem	onesuc 7243	Exponentiation with a successor exponent. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by Mario Carneiro, 14-Nov-2014.)
|- ( ( A e. On /\ B e. om ) -> ( A ^o suc B ) = ( ( A ^o B ) .o A ) )
Theorem	oa1suc 7244	Addition with 1 is same as successor. Proposition 4.34(a) of [Mendelson] p. 266. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro, 16-Nov-2014.)
|- ( A e. On -> ( A +o 1o ) = suc A )
Theorem	oalim 7245*	Ordinal addition with a limit ordinal. Definition 8.1 of [TakeutiZaring] p. 56. (Contributed by NM, 3-Aug-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A +o B ) = U_ x e. B ( A +o x ) )
Theorem	omlim 7246*	Ordinal multiplication with a limit ordinal. Definition 8.15 of [TakeutiZaring] p. 62. (Contributed by NM, 3-Aug-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A .o B ) = U_ x e. B ( A .o x ) )
Theorem	oelim 7247*	Ordinal exponentiation with a limit exponent and nonzero mantissa. Definition 8.30 of [TakeutiZaring] p. 67. (Contributed by NM, 1-Jan-2005.) (Revised by Mario Carneiro, 8-Sep-2013.)
|- ( ( ( A e. On /\ ( B e. C /\ Lim B ) ) /\ (/) e. A ) -> ( A ^o B ) = U_ x e. B ( A ^o x ) )
Theorem	oacl 7248	Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.)
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
Theorem	omcl 7249	Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57. (Contributed by NM, 3-Aug-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On )
Theorem	oecl 7250	Closure law for ordinal exponentiation. (Contributed by NM, 1-Jan-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
Theorem	oa0r 7251	Ordinal addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.)
|- ( A e. On -> ( (/) +o A ) = A )
Theorem	om0r 7252	Ordinal multiplication with zero. Proposition 8.18(1) of [TakeutiZaring] p. 63. (Contributed by NM, 3-Aug-2004.)
|- ( A e. On -> ( (/) .o A ) = (/) )
Theorem	o1p1e2 7253	1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
|- ( 1o +o 1o ) = 2o
Theorem	om1 7254	Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63. (Contributed by NM, 29-Oct-1995.)
|- ( A e. On -> ( A .o 1o ) = A )
Theorem	om1r 7255	Ordinal multiplication with 1. Proposition 8.18(2) of [TakeutiZaring] p. 63. (Contributed by NM, 3-Aug-2004.)
|- ( A e. On -> ( 1o .o A ) = A )
Theorem	oe1 7256	Ordinal exponentiation with an exponent of 1. (Contributed by NM, 2-Jan-2005.)
|- ( A e. On -> ( A ^o 1o ) = A )
Theorem	oe1m 7257	Ordinal exponentiation with a mantissa of 1. Proposition 8.31(3) of [TakeutiZaring] p. 67. (Contributed by NM, 2-Jan-2005.)
|- ( A e. On -> ( 1o ^o A ) = 1o )
Theorem	oaordi 7258	Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58. (Contributed by NM, 5-Dec-2004.)
|- ( ( B e. On /\ C e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
Theorem	oaord 7259	Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58 and its converse. (Contributed by NM, 5-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A e. B <-> ( C +o A ) e. ( C +o B ) ) )
Theorem	oacan 7260	Left cancellation law for ordinal addition. Corollary 8.5 of [TakeutiZaring] p. 58. (Contributed by NM, 5-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +o B ) = ( A +o C ) <-> B = C ) )
Theorem	oaword 7261	Weak ordering property of ordinal addition. (Contributed by NM, 6-Dec-2004.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B <-> ( C +o A ) C_ ( C +o B ) ) )
Theorem	oawordri 7262	Weak ordering property of ordinal addition. Proposition 8.7 of [TakeutiZaring] p. 59. (Contributed by NM, 7-Dec-2004.)
|- ( ( A e. On /\ B e. On /\ C e. On ) -> ( A C_ B -> ( A +o C ) C_ ( B +o C ) ) )
Theorem	oaord1 7263	An ordinal is less than its sum with a nonzero ordinal. Theorem 18 of [Suppes] p. 209 and its converse. (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( (/) e. B <-> A e. ( A +o B ) ) )
Theorem	oaword1 7264	An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (For the other part see oaord1 7263.) (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
Theorem	oaword2 7265	An ordinal is less than or equal to its sum with another. Theorem 21 of [Suppes] p. 209. (Contributed by NM, 7-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> A C_ ( B +o A ) )
Theorem	oawordeulem 7266*	Lemma for oawordex 7269. (Contributed by NM, 11-Dec-2004.)
|- A e. On   &    |- B e. On   &    |- S = { y e. On | B C_ ( A +o y ) }   =>    |- ( A C_ B -> E! x e. On ( A +o x ) = B )
Theorem	oawordeu 7267*	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59. (Contributed by NM, 11-Dec-2004.)
|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> E! x e. On ( A +o x ) = B )
Theorem	oawordexr 7268*	Existence theorem for weak ordering of ordinal sum. (Contributed by NM, 12-Dec-2004.)
|- ( ( A e. On /\ E. x e. On ( A +o x ) = B ) -> A C_ B )
Theorem	oawordex 7269*	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59 and its converse. See oawordeu 7267 for uniqueness. (Contributed by NM, 12-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( A C_ B <-> E. x e. On ( A +o x ) = B ) )
Theorem	oaordex 7270*	Existence theorem for ordering of ordinal sum. Similar to Proposition 4.34(f) of [Mendelson] p. 266 and its converse. (Contributed by NM, 12-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( A e. B <-> E. x e. On ( (/) e. x /\ ( A +o x ) = B ) ) )
Theorem	oa00 7271	An ordinal sum is zero iff both of its arguments are zero. (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) = (/) <-> ( A = (/) /\ B = (/) ) ) )
Theorem	oalimcl 7272	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 7273	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 7274*	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 7275*	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 7276*	Lemma for oacomf1o 7277. (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 7277*	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 8165). (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 7278	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 7279	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 7280	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 7281	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 7282	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 7283	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 7284	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 7285	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 7286	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 7287	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 7288	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 7289*	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 7290	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 7291	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 7292	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 7293	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 7294*	Lemma for omeu 7297: 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 7295	Lemma for omeu 7297: 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 7296	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 7297*	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 7298	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 7299	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 7300	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 ) ) )