Theorem o1p1e2

Description: 1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004)

	Ref	Expression
Assertion	o1p1e2	|- ( 1o +o 1o ) = 2o

Proof

Step	Hyp	Ref	Expression
1		1on	|- 1o e. On
2		oa1suc	|- ( 1o e. On -> ( 1o +o 1o ) = suc 1o )
3	1 2	ax-mp	|- ( 1o +o 1o ) = suc 1o
4		df-2o	|- 2o = suc 1o
5	3 4	eqtr4i	|- ( 1o +o 1o ) = 2o