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 ∈ On
2		oa1suc	⊢ ( 1o ∈ 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