P. 60 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 5901-6000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rdgtfr 5901*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.)
|- ((A.z( F ` z) e. _V /\ A e. V) -> ( Fun (g e. _V |-> (A u. U_x e. dom g( F ` (g ` x)))) /\ ((g e. _V |-> (A u. U_x e. dom g( F ` (g ` x)))) ` f) e. _V))
Theorem	rdgruledefgg 5902*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
|- (( F Fn _V /\ A e. V) -> ( Fun (g e. _V |-> (A u. U_x e. dom g( F ` (g ` x)))) /\ ((g e. _V |-> (A u. U_x e. dom g( F ` (g ` x)))) ` f) e. _V))
Theorem	rdgruledefg 5903*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
|- F Fn _V   =>   |- (A e. V -> ( Fun (g e. _V |-> (A u. U_x e. dom g( F ` (g ` x)))) /\ ((g e. _V |-> (A u. U_x e. dom g( F ` (g ` x)))) ` f) e. _V))
Theorem	rdgexggg 5904	The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
|- (( F Fn _V /\ A e. V /\ B e. W) -> ( rec( F , A) ` B) e. _V)
Theorem	rdgexgg 5905	The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
|- F Fn _V   =>   |- ((A e. V /\ B e. W) -> ( rec( F , A) ` B) e. _V)
Theorem	rdgifnon 5906	The recursive definition generator is a function on ordinal numbers. The F Fn _V condition states that the characteristic function is defined for all sets (being defined for all ordinals might be enough if being used in a manner similar to rdgon 5913; in cases like df-oadd 5944 either presumably could work). (Contributed by Jim Kingdon, 13-Jul-2019.)
|- (( F Fn _V /\ A e. V) -> rec( F , A) Fn On)
Theorem	rdgifnon2 5907*	The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.)
|- ((A.z( F ` z) e. _V /\ A e. V) -> rec( F , A) Fn On)
Theorem	rdgivallem 5908*	Value of the recursive definition generator. Lemma for rdgival 5909 which simplifies the value further. (Contributed by Jim Kingdon, 13-Jul-2019.) (New usage is discouraged.)
|- (( F Fn _V /\ A e. V /\ B e. On) -> ( rec( F , A) ` B) = (A u. U_x e. B ( F ` (( rec( F , A) |` B) ` x))))
Theorem	rdgival 5909*	Value of the recursive definition generator. (Contributed by Jim Kingdon, 26-Jul-2019.)
|- (( F Fn _V /\ A e. V /\ B e. On) -> ( rec( F , A) ` B) = (A u. U_x e. B ( F ` ( rec( F , A) ` x))))
Theorem	rdgss 5910	Subset and recursive definition generator. (Contributed by Jim Kingdon, 15-Jul-2019.)
|- (ph -> F Fn _V)   &   |- (ph -> I e. V)   &   |- (ph -> A e. On)   &   |- (ph -> B e. On)   &   |- (ph -> A C_ B)   =>   |- (ph -> ( rec( F , I) ` A) C_ ( rec( F , I) ` B))
Theorem	rdgisuc1 5911*	One way of describing the value of the recursive definition generator at a successor. There is no condition on the characteristic function F other than F Fn _V. Given that, the resulting expression encompasses both the expected successor term ( F ` ( rec( F , A) ` B)) but also terms that correspond to the initial value A and to limit ordinals U_x e. B( F ` ( rec( F , A) ` x)). If we add conditions on the characteristic function, we can show tighter results such as rdgisucinc 5912. (Contributed by Jim Kingdon, 9-Jun-2019.)
|- (ph -> F Fn _V)   &   |- (ph -> A e. V)   &   |- (ph -> B e. On)   =>   |- (ph -> ( rec( F , A) ` suc B) = (A u. ( U_x e. B ( F ` ( rec( F , A) ` x)) u. ( F ` ( rec( F , A) ` B)))))
Theorem	rdgisucinc 5912*	Value of the recursive definition generator at a successor. This can be thought of as a generalization of oasuc 5983 and omsuc 5990. (Contributed by Jim Kingdon, 29-Aug-2019.)
|- (ph -> F Fn _V)   &   |- (ph -> A e. V)   &   |- (ph -> B e. On)   &   |- (ph -> A.x x C_ ( F ` x))   =>   |- (ph -> ( rec( F , A) ` suc B) = ( F ` ( rec( F , A) ` B)))
Theorem	rdgon 5913*	Evaluating the recursive definition generator produces an ordinal. There is a hypothesis that the characteristic function produces ordinals on ordinal arguments. (Contributed by Jim Kingdon, 26-Jul-2019.)
|- (ph -> F Fn _V)   &   |- (ph -> A e. On)   &   |- (ph -> A.x e. On ( F ` x) e. On)   =>   |- ((ph /\ B e. On) -> ( rec( F , A) ` B) e. On)
Theorem	rdg0 5914	The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- A e. _V   =>   |- ( rec( F , A) ` (/)) = A
Theorem	rdg0g 5915	The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.)
|- (A e. C -> ( rec( F , A) ` (/)) = A)
Theorem	rdgexg 5916	The recursive definition generator produces a set on a set input. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- A e. _V   &   |- F Fn _V   =>   |- (B e. V -> ( rec( F , A) ` B) e. _V)
2.6.21  Finite recursion
Syntax	cfrec 5917	Extend class notation with the fnite recursive definition generator, with characteristic function F and initial value I.
class frec( F , I)
Definition	df-frec 5918*	Define a recursive definition generator on om (the class of finite ordinals) with characteristic function F and initial value I. This rather amazing operation allows us to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the daunting complexity of our frec operation (especially when df-recs 5861 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple; see frec0g 5922 and frecsuc 5930. Unlike with transfinite recursion, finite recurson can readily divide definitions and proofs into zero and successor cases, because even without excluded middle we have theorems such as nn0suc 4270. The analogous situation with transfinite recursion - being able to say that an ordinal is zero, successor, or limit - is enabled by excluded middle and thus is not available to us. For the characteristic functions which satisfy the conditions given at frecrdg 5931, this definition and df-irdg 5897 restricted to om produce the same result. Note: We introduce frec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Mario Carneiro and Jim Kingdon, 10-Aug-2019.)
|- frec( F , I) = (recs((g e. _V |-> {x | (E. m e. om ( dom g = suc m /\ x e. ( F ` (g ` m))) \/ ( dom g = (/) /\ x e. I)) })) |` om)
Theorem	freceq1 5919	Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( F = G -> frec( F , A) = frec( G , A))
Theorem	freceq2 5920	Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- (A = B -> frec( F , A) = frec( F , B))
Theorem	nffrec 5921	Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- F/_x F   &   |- F/_xA   =>   |- F/_xfrec( F , A)
Theorem	frec0g 5922	The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.)
|- (A e. V -> (frec( F , A) ` (/)) = A)
Theorem	frecabex 5923*	The class abstraction from df-frec 5918 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.)
|- (ph -> S e. V)   &   |- (ph -> A.y( F ` y) e. _V)   &   |- (ph -> A e. W)   =>   |- (ph -> {x | (E. m e. om ( dom S = suc m /\ x e. ( F ` ( S ` m))) \/ ( dom S = (/) /\ x e. A)) } e. _V)
Theorem	frectfr 5924*	Lemma to connect transfinite recursion theorems with finite recursion. That is, given the conditions F Fn _V and A e. V on frec( F , A), we want to be able to apply tfri1d 5890 or tfri2d 5891, and this lemma lets us satisfy hypotheses of those theorems. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- G = (g e. _V |-> {x | (E. m e. om ( dom g = suc m /\ x e. ( F ` (g ` m))) \/ ( dom g = (/) /\ x e. A)) })   =>   |- ((A.z( F ` z) e. _V /\ A e. V) -> A.y( Fun G /\ ( G ` y) e. _V))
Theorem	frecfnom 5925*	The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.)
|- ((A.z( F ` z) e. _V /\ A e. V) -> frec( F , A) Fn om)
Theorem	frecsuclem1 5926*	Lemma for frecsuc 5930. (Contributed by Jim Kingdon, 13-Aug-2019.)
|- G = (g e. _V |-> {x | (E. m e. om ( dom g = suc m /\ x e. ( F ` (g ` m))) \/ ( dom g = (/) /\ x e. A)) })   =>   |- ((A.z( F ` z) e. _V /\ A e. V /\ B e. om) -> (frec( F , A) ` suc B) = ( G ` (recs( G) |` suc B)))
Theorem	frecsuclemdm 5927*	Lemma for frecsuc 5930. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- G = (g e. _V |-> {x | (E. m e. om ( dom g = suc m /\ x e. ( F ` (g ` m))) \/ ( dom g = (/) /\ x e. A)) })   =>   |- ((A.z( F ` z) e. _V /\ A e. V /\ B e. om) -> dom (recs( G) |` suc B) = suc B)
Theorem	frecsuclem2 5928*	Lemma for frecsuc 5930. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- G = (g e. _V |-> {x | (E. m e. om ( dom g = suc m /\ x e. ( F ` (g ` m))) \/ ( dom g = (/) /\ x e. A)) })   =>   |- ((A.z( F ` z) e. _V /\ A e. V /\ B e. om) -> ((recs( G) |` suc B) ` B) = (frec( F , A) ` B))
Theorem	frecsuclem3 5929*	Lemma for frecsuc 5930. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- G = (g e. _V |-> {x | (E. m e. om ( dom g = suc m /\ x e. ( F ` (g ` m))) \/ ( dom g = (/) /\ x e. A)) })   =>   |- ((A.z( F ` z) e. _V /\ A e. V /\ B e. om) -> (frec( F , A) ` suc B) = ( F ` (frec( F , A) ` B)))
Theorem	frecsuc 5930*	The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- ((A.z( F ` z) e. _V /\ A e. V /\ B e. om) -> (frec( F , A) ` suc B) = ( F ` (frec( F , A) ` B)))
Theorem	frecrdg 5931*	Transfinite recursion restricted to omega. Given a suitable characteristic function, df-frec 5918 produces the same results as df-irdg 5897 restricted to om. Presumably the theorem would also hold if F Fn _V were changed to A.z( F ` z) e. _V. (Contributed by Jim Kingdon, 29-Aug-2019.)
|- (ph -> F Fn _V)   &   |- (ph -> A e. V)   &   |- (ph -> A.x x C_ ( F ` x))   =>   |- (ph -> frec( F , A) = ( rec( F , A) |` om))
Theorem	freccl 5932*	Closure for finite recursion. (Contributed by Jim Kingdon, 25-May-2020.)
|- (ph -> A.z( F ` z) e. _V)   &   |- (ph -> A e. S)   &   |- ((ph /\ z e. S) -> ( F ` z) e. S)   &   |- (ph -> B e. om)   =>   |- (ph -> (frec( F , A) ` B) e. S)
2.6.22  Ordinal arithmetic
Syntax	c1o 5933	Extend the definition of a class to include the ordinal number 1.
class 1o
Syntax	c2o 5934	Extend the definition of a class to include the ordinal number 2.
class 2o
Syntax	c3o 5935	Extend the definition of a class to include the ordinal number 3.
class 3o
Syntax	c4o 5936	Extend the definition of a class to include the ordinal number 4.
class 4o
Syntax	coa 5937	Extend the definition of a class to include the ordinal addition operation.
class +o
Syntax	comu 5938	Extend the definition of a class to include the ordinal multiplication operation.
class .o
Syntax	coei 5939	Extend the definition of a class to include the ordinal exponentiation operation.
class ↑𝑜
Definition	df-1o 5940	Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)
|- 1o = suc (/)
Definition	df-2o 5941	Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)
|- 2o = suc 1o
Definition	df-3o 5942	Define the ordinal number 3. (Contributed by Mario Carneiro, 14-Jul-2013.)
|- 3o = suc 2o
Definition	df-4o 5943	Define the ordinal number 4. (Contributed by Mario Carneiro, 14-Jul-2013.)
|- 4o = suc 3o
Definition	df-oadd 5944*	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 5945*	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-oexpi 5946*	Define the ordinal exponentiation operation. This definition is similar to a conventional definition of exponentiation except that it defines (/) ↑𝑜 A to be 1o for all A e. On, in order to avoid having different cases for whether the base is (/) or not. (Contributed by Mario Carneiro, 4-Jul-2019.)
|- ↑𝑜 = (x e. On , y e. On |-> ( rec((z e. _V |-> (z .o x)) , 1o) ` y))
Theorem	1on 5947	Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995.)
|- 1o e. On
Theorem	2on 5948	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 5949	Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.)
|- 2o =/= (/)
Theorem	3on 5950	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 3o e. On
Theorem	4on 5951	Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- 4o e. On
Theorem	df1o2 5952	Expanded value of the ordinal number 1. (Contributed by NM, 4-Nov-2002.)
|- 1o = { (/) }
Theorem	df2o3 5953	Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- 2o = { (/) , 1o }
Theorem	df2o2 5954	Expanded value of the ordinal number 2. (Contributed by NM, 29-Jan-2004.)
|- 2o = { (/) , { (/) } }
Theorem	1n0 5955	Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)
|- 1o =/= (/)
Theorem	xp01disj 5956	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 5957	Two ways to express that an ordinal class is positive. (Contributed by NM, 21-Dec-2004.)
|- ( Ord A -> ( (/) e. A <-> 1o C_ A))
Theorem	ordge1n0im 5958	An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim Kingdon, 26-Jun-2019.)
|- ( Ord A -> ( 1o C_ A -> A =/= (/)))
Theorem	el1o 5959	Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)
|- (A e. 1o <-> A = (/))
Theorem	dif1o 5960	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	2oconcl 5961	Closure of the pair swapping function on 2o. (Contributed by Mario Carneiro, 27-Sep-2015.)
|- (A e. 2o -> ( 1o \ A) e. 2o)
Theorem	0lt1o 5962	Ordinal zero is less than ordinal one. (Contributed by NM, 5-Jan-2005.)
|- (/) e. 1o
Theorem	oafnex 5963	The characteristic function for ordinal addition is defined everywhere. (Contributed by Jim Kingdon, 27-Jul-2019.)
|- (x e. _V |-> suc x) Fn _V
Theorem	sucinc 5964*	Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.)
|- F = (z e. _V |-> suc z)   =>   |- A.x x C_ ( F ` x)
Theorem	sucinc2 5965*	Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.)
|- F = (z e. _V |-> suc z)   =>   |- ((B e. On /\ A e. B) -> ( F ` A) C_ ( F ` B))
Theorem	fnoa 5966	Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.)
|- +o Fn ( On X. On)
Theorem	oaexg 5967	Ordinal addition is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- ((A e. V /\ B e. W) -> (A +o B) e. _V)
Theorem	omfnex 5968*	The characteristic function for ordinal multiplication is defined everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.)
|- (A e. V -> (x e. _V |-> (x +o A)) Fn _V)
Theorem	fnom 5969	Functionality and domain of ordinal multiplication. (Contributed by NM, 26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.)
|- .o Fn ( On X. On)
Theorem	omexg 5970	Ordinal multiplication is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- ((A e. V /\ B e. W) -> (A .o B) e. _V)
Theorem	fnoei 5971	Functionality and domain of ordinal exponentiation. (Contributed by Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro, 3-Jul-2019.)
|- ↑𝑜 Fn ( On X. On)
Theorem	oeiexg 5972	Ordinal exponentiation is a set. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- ((A e. V /\ B e. W) -> (A ↑𝑜 B) e. _V)
Theorem	oav 5973*	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 5974*	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	oeiv 5975*	Value of ordinal exponentiation. (Contributed by Jim Kingdon, 9-Jul-2019.)
|- ((A e. On /\ B e. On) -> (A ↑𝑜 B) = ( rec((x e. _V |-> (x .o A)) , 1o) ` B))
Theorem	oa0 5976	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 5977	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	oei0 5978	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 ↑𝑜 (/)) = 1o)
Theorem	oacl 5979	Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring] p. 57. (Contributed by NM, 5-May-1995.) (Constructive proof by Jim Kingdon, 26-Jul-2019.)
|- ((A e. On /\ B e. On) -> (A +o B) e. On)
Theorem	omcl 5980	Closure law for ordinal multiplication. Proposition 8.16 of [TakeutiZaring] p. 57. (Contributed by NM, 3-Aug-2004.) (Constructive proof by Jim Kingdon, 26-Jul-2019.)
|- ((A e. On /\ B e. On) -> (A .o B) e. On)
Theorem	oeicl 5981	Closure law for ordinal exponentiation. (Contributed by Jim Kingdon, 26-Jul-2019.)
|- ((A e. On /\ B e. On) -> (A ↑𝑜 B) e. On)
Theorem	oav2 5982*	Value of ordinal addition. (Contributed by Mario Carneiro and Jim Kingdon, 12-Aug-2019.)
|- ((A e. On /\ B e. On) -> (A +o B) = (A u. U_x e. B suc (A +o x)))
Theorem	oasuc 5983	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	omv2 5984*	Value of ordinal multiplication. (Contributed by Jim Kingdon, 23-Aug-2019.)
|- ((A e. On /\ B e. On) -> (A .o B) = U_x e. B ((A .o x) +o A))
Theorem	onasuc 5985	Addition with successor. Theorem 4I(A2) of [Enderton] p. 79. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- ((A e. On /\ B e. om) -> (A +o suc B) = suc (A +o B))
Theorem	oa1suc 5986	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	o1p1e2 5987	1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
|- ( 1o +o 1o) = 2o
Theorem	oawordi 5988	Weak ordering property of ordinal addition. (Contributed by Jim Kingdon, 27-Jul-2019.)
|- ((A e. On /\ B e. On /\ C e. On) -> (A C_ B -> ( C +o A) C_ ( C +o B)))
Theorem	oaword1 5989	An ordinal is less than or equal to its sum with another. Part of Exercise 5 of [TakeutiZaring] p. 62. (Contributed by NM, 6-Dec-2004.)
|- ((A e. On /\ B e. On) -> A C_ (A +o B))
Theorem	omsuc 5990	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	onmsuc 5991	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))
2.6.23  Natural number arithmetic
Theorem	nna0 5992	Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by NM, 20-Sep-1995.)
|- (A e. om -> (A +o (/)) = A)
Theorem	nnm0 5993	Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80. (Contributed by NM, 20-Sep-1995.)
|- (A e. om -> (A .o (/)) = (/))
Theorem	nnasuc 5994	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 5995	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	nna0r 5996	Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- (A e. om -> ( (/) +o A) = A)
Theorem	nnm0r 5997	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 5998	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 5999	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	nnacli 6000	om is closed under addition. Inference form of nnacl 5998. (Contributed by Scott Fenton, 20-Apr-2012.)
|- A e. om   &   |- B e. om   =>   |- (A +o B) e. om