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

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 𝑜