Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Natural number arithmetic
4onn
Next ⟩
1one2o
Metamath Proof Explorer
Ascii
Unicode
Theorem
4onn
Description:
The ordinal 4 is a natural number.
(Contributed by
Mario Carneiro
, 5-Jan-2016)
Ref
Expression
Assertion
4onn
⊢
4
𝑜
∈
ω
Proof
Step
Hyp
Ref
Expression
1
df-4o
⊢
4
𝑜
=
suc
⁡
3
𝑜
2
3onn
⊢
3
𝑜
∈
ω
3
peano2
⊢
3
𝑜
∈
ω
→
suc
⁡
3
𝑜
∈
ω
4
2
3
ax-mp
⊢
suc
⁡
3
𝑜
∈
ω
5
1
4
eqeltri
⊢
4
𝑜
∈
ω