Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
The natural numbers (i.e., finite ordinals)
omelon2
Next ⟩
nnlim
Metamath Proof Explorer
Ascii
Unicode
Theorem
omelon2
Description:
Omega is an ordinal number.
(Contributed by
Mario Carneiro
, 30-Jan-2013)
Ref
Expression
Assertion
omelon2
⊢
ω
∈
V
→
ω
∈
On
Proof
Step
Hyp
Ref
Expression
1
omon
⊢
ω
∈
On
∨
ω
=
On
2
1
ori
⊢
¬
ω
∈
On
→
ω
=
On
3
onprc
⊢
¬
On
∈
V
4
eleq1
⊢
ω
=
On
→
ω
∈
V
↔
On
∈
V
5
3
4
mtbiri
⊢
ω
=
On
→
¬
ω
∈
V
6
2
5
syl
⊢
¬
ω
∈
On
→
¬
ω
∈
V
7
6
con4i
⊢
ω
∈
V
→
ω
∈
On