Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
ord3
Next ⟩
3on
Metamath Proof Explorer
Ascii
Unicode
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
𝑜