Metamath Proof Explorer
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 ) |