Theorem omsson 7811

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

Assertion

Ref	Expression
omsson	⊢ ω ⊆ On

Proof of Theorem omsson

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-om 7808	. 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
2	1	ssrab3 4045	1 ⊢ ω ⊆ On

Syntax hints:   → wi 4  ∀wal 1539   ⊆ wss 3913  Oncon0 6322  Lim wlim 6323  ωcom 7807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930  df-om 7808

This theorem is referenced by:  limomss  7812  nnon  7813  ordom  7817  omssnlim  7822  omsinds  7828  omsindsOLD  7829  nnunifi  9245  unblem1  9246  unblem2  9247  unblem3  9248  unblem4  9249  isfinite2  9252  card2inf  9500  ackbij1lem16  10180  ackbij1lem18  10182  fin23lem26  10270  fin23lem27  10273  isf32lem5  10302  fin1a2lem6  10350  pwfseqlem3  10605  tskinf  10714  grothomex  10774  ltsopi  10833  dmaddpi  10835  dmmulpi  10836  2ndcdisj  22844  finminlem  34866  cantnftermord  41713  omabs2  41725