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

Metamath Proof Explorer

Theorem 2on0

Description: Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011)

		Ref	Expression
	Assertion	2on0	$⊢ 2_{𝑜} \neq \emptyset$

Step	Hyp	Ref	Expression
1		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
2		nsuceq0	$⊢ suc 1_{𝑜} \neq \emptyset$
3	1 2	eqnetri	$⊢ 2_{𝑜} \neq \emptyset$