ord3

Description: Ordinal 3 is an ordinal class. (Contributed by BTernaryTau, 6-Jan-2025)

		Ref	Expression
	Assertion	ord3	$⊢ Ord 3_{𝑜}$

Step	Hyp	Ref	Expression
1		2on	$⊢ 2_{𝑜} \in On$
2		eloni	$⊢ 2_{𝑜} \in On \to Ord 2_{𝑜}$
3		ordsuci	$⊢ Ord 2_{𝑜} \to Ord suc 2_{𝑜}$
4	1 2 3	mp2b	$⊢ Ord suc 2_{𝑜}$
5		df-3o	$⊢ 3_{𝑜} = suc 2_{𝑜}$
6		ordeq	$⊢ 3_{𝑜} = suc 2_{𝑜} \to (Ord 3_{𝑜} \leftrightarrow Ord suc 2_{𝑜})$
7	5 6	ax-mp	$⊢ Ord 3_{𝑜} \leftrightarrow Ord suc 2_{𝑜}$
8	4 7	mpbir	$⊢ Ord 3_{𝑜}$

Metamath Proof Explorer