Metamath Proof Explorer


Theorem omsson

Description: Omega is a subset of On . (Contributed by NM, 13-Jun-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion omsson ω On

Proof

Step Hyp Ref Expression
1 df-om ω = x On | y Lim y x y
2 1 ssrab3 ω On