Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Ordinal arithmetic
3on
Next ⟩
4on
Metamath Proof Explorer
Ascii
Unicode
Theorem
3on
Description:
Ordinal 3 is an ordinal number.
(Contributed by
Mario Carneiro
, 5-Jan-2016)
Ref
Expression
Assertion
3on
⊢
3
𝑜
∈
On
Proof
Step
Hyp
Ref
Expression
1
df-3o
⊢
3
𝑜
=
suc
⁡
2
𝑜
2
2on
⊢
2
𝑜
∈
On
3
2
onsuci
⊢
suc
⁡
2
𝑜
∈
On
4
1
3
eqeltri
⊢
3
𝑜
∈
On