This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem o1p1e2

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

		Ref	Expression
	Assertion	o1p1e2	$⊢ 1_{𝑜} +_{𝑜} 1_{𝑜} = 2_{𝑜}$

Step	Hyp	Ref	Expression
1		1on	$⊢ 1_{𝑜} \in On$
2		oa1suc	$⊢ 1_{𝑜} \in On \to 1_{𝑜} +_{𝑜} 1_{𝑜} = suc 1_{𝑜}$
3	1 2	ax-mp	$⊢ 1_{𝑜} +_{𝑜} 1_{𝑜} = suc 1_{𝑜}$
4		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
5	3 4	eqtr4i	$⊢ 1_{𝑜} +_{𝑜} 1_{𝑜} = 2_{𝑜}$