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 
|- _om C_ On

Proof

Step Hyp Ref Expression
1 dfom2 
 |-  _om = { x e. On | suc x C_ { y e. On | -. Lim y } }
2 1 ssrab3 
 |-  _om C_ On