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	seqomlem4 7201*	Lemma for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 23-Jun-2015.)
|- Q = rec ( ( i e. om , v e. _V |-> <. suc i , ( i F v ) >. ) , <. (/) , ( _I ` I ) >. )   =>    |- ( A e. om -> ( ( Q " om ) ` suc A ) = ( A F ( ( Q " om ) ` A ) ) )
Theorem	seqomeq12 7202	Equality theorem for seq𝜔. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- ( ( A = B /\ C = D ) -> seq𝜔 ( A , C ) = seq𝜔 ( B , D ) )
Theorem	fnseqom 7203	An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- G = seq𝜔 ( F , I )   =>    |- G Fn om
Theorem	seqom0g 7204	Value of an index-aware recursive definition at 0. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- G = seq𝜔 ( F , I )   =>    |- ( I e. _V -> ( G ` (/) ) = I )
Theorem	seqomsuc 7205	Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014.)
|- G = seq𝜔 ( F , I )   =>    |- ( A e. om -> ( G ` suc A ) = ( A F ( G ` A ) ) )
2.4.18  Ordinal arithmetic
Syntax	c1o 7206	Extend the definition of a class to include the ordinal number 1.
class 1o
Syntax	c2o 7207	Extend the definition of a class to include the ordinal number 2.
class 2o
Syntax	c3o 7208	Extend the definition of a class to include the ordinal number 3.
class 3o
Syntax	c4o 7209	Extend the definition of a class to include the ordinal number 4.
class 4o
Syntax	coa 7210	Extend the definition of a class to include the ordinal addition operation.
class +o
Syntax	comu 7211	Extend the definition of a class to include the ordinal multiplication operation.
class .o
Syntax	coe 7212	Extend the definition of a class to include the ordinal exponentiation operation.
class ^o
Definition	df-1o 7213	Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)
|- 1o = suc (/)
Definition	df-2o 7214	Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)
|- 2o = suc 1o
Definition	df-3o 7215	Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.)
|- 3o = suc 2o
Definition	df-4o 7216	Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.)
|- 4o = suc 3o
Definition	df-oadd 7217*	Define the ordinal addition operation. (Contributed by NM, 3-May-1995.)
|- +o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> suc z ) , x ) ` y ) )
Definition	df-omul 7218*	Define the ordinal multiplication operation. (Contributed by NM, 26-Aug-1995.)
|- .o = ( x e. On , y e. On |-> ( rec ( ( z e. _V |-> ( z +o x ) ) , (/) ) ` y ) )
Definition	df-oexp 7219*	Define the ordinal exponentiation operation. (Contributed by NM, 30-Dec-2004.)
|- ^o = ( x e. On , y e. On |-> if ( x = (/) , ( 1o \ y ) , ( rec ( ( z e. _V |-> ( z .o x ) ) , 1o ) ` y ) ) )
Theorem	1on 7220	Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. On
Theorem	2on 7221	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 7222	Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.)
|- 2o =/= (/)
Theorem	3on 7223	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. On
Theorem	4on 7224	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. On
Theorem	df1o2 7225	Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
|- 1o = { (/) }
Theorem	df2o3 7226	Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- 2o = { (/) , 1o }
Theorem	df2o2 7227	Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.)
|- 2o = { (/) , { (/) } }
Theorem	1n0 7228	Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)
|- 1o =/= (/)
Theorem	xp01disj 7229	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 7230	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 7231	An ordinal greater than or equal to 1 is nonzero. (Contributed by NM, 21-Dec-2004.)
|- ( Ord A -> ( 1o C_ A <-> A =/= (/) ) )
Theorem	el1o 7232	Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)
|- ( A e. 1o <-> A = (/) )
Theorem	dif1o 7233	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 7234	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 7235	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 7236	Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- ( A e. 2o -> ( 1o \ A ) e. 2o )
Theorem	0lt1o 7237	Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)
|- (/) e. 1o
Theorem	dif20el 7238	An ordinal greater than one is greater than zero. (Contributed by Mario Carneiro, 25-May-2015.)
|- ( A e. ( On \ 2o ) -> (/) e. A )
Theorem	0we1 7239	The empty set is a well-ordering of ordinal one. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- (/) We 1o
Theorem	brwitnlem 7240	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 7241	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 7242	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 7243	Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.)
|- ^o Fn ( On X. On )
Theorem	oav 7244*	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 7245*	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 7246	A helper lemma for oe0 7255 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 7247*	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 7248*	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 7249	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 7250	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 7251	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 7252	Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring] p. 62. Unlike om0 7250, 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 7253	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 7254	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 7255	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 7256*	Alternate value of ordinal exponentiation. Compare oev 7247. (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 7257	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 7258*	Lemma for oesuc 7260. (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 7259	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 7260	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 7261	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Note that this version of oasuc 7257 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 7262	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 7263	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 7264	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 7265*	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 7266*	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 7267*	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 7268	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 7269	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 7270	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 7271	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 7272	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 7273	1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
|- ( 1o +o 1o ) = 2o
Theorem	om1 7274	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 7275	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 7276	Ordinal exponentiation with an exponent of 1. (Contributed by NM, 2-Jan-2005.)
|- ( A e. On -> ( A ^o 1o ) = A )
Theorem	oe1m 7277	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 7278	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 7279	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 7280	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 7281	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 7282	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 7283	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 7284	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 7283.) (Contributed by NM, 6-Dec-2004.)
|- ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
Theorem	oaword2 7285	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 7286*	Lemma for oawordex 7289. (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 7287*	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 7288*	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 7289*	Existence theorem for weak ordering of ordinal sum. Proposition 8.8 of [TakeutiZaring] p. 59 and its converse. See oawordeu 7287 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 7290*	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 7291	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 7292	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 7293	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 7294*	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 7295*	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 7296*	Lemma for oacomf1o 7297. (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 7297*	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 8187). (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 7298	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 7299	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 7300	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 ) ) )