Metamath Proof Explorer


Theorem ord3

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

Ref Expression
Assertion ord3 Ord 3 𝑜

Proof

Step Hyp Ref Expression
1 2on 2 𝑜 On
2 eloni 2 𝑜 On Ord 2 𝑜
3 ordsuci Ord 2 𝑜 Ord suc 2 𝑜
4 1 2 3 mp2b Ord suc 2 𝑜
5 df-3o 3 𝑜 = suc 2 𝑜
6 ordeq 3 𝑜 = suc 2 𝑜 Ord 3 𝑜 Ord suc 2 𝑜
7 5 6 ax-mp Ord 3 𝑜 Ord suc 2 𝑜
8 4 7 mpbir Ord 3 𝑜