Theorem ord3

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

	Ref	Expression
Assertion	ord3	|- Ord 3o

Proof

Step	Hyp	Ref	Expression
1		2on	|- 2o e. On
2		eloni	|- ( 2o e. On -> Ord 2o )
3		ordsuci	|- ( Ord 2o -> Ord suc 2o )
4	1 2 3	mp2b	|- Ord suc 2o
5		df-3o	|- 3o = suc 2o
6		ordeq	|- ( 3o = suc 2o -> ( Ord 3o <-> Ord suc 2o ) )
7	5 6	ax-mp	|- ( Ord 3o <-> Ord suc 2o )
8	4 7	mpbir	|- Ord 3o