Metamath Proof Explorer


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 ∈ On
2 eloni ( 2o ∈ 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