Description: Ordinal 3 is an ordinal class. (Contributed by BTernaryTau, 6-Jan-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | ord3 | ⊢ Ord 3o |
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 |