Theorem omsson 7867

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 7864	. 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)}
2	1	ssrab3 4037	1 ⊢ ω ⊆ On

Syntax hints:   → wi 4  ∀wal 1568   ⊆ wss 3906  Oncon0 6362  Lim wlim 6363  ωcom 7863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3923  df-om 7864

This theorem is referenced by:  limomss  7868  nnon  7869  ordom  7873  omssnlim  7878  omsinds  7884  nnunifi  9252  unblem1  9253  unblem2  9254  unblem3  9255  unblem4  9256  isfinite2  9259  card2inf  9518  ackbij1lem16  10218  ackbij1lem18  10220  fin23lem26  10310  fin23lem27  10313  isf32lem5  10342  fin1a2lem6  10390  pwfseqlem3  10646  tskinf  10755  grothomex  10815  ltsopi  10874  dmaddpi  10876  dmmulpi  10877  2ndcdisj  23594  finminlem  36807  ttcid  36981  dfttc2g  36995  cantnftermord  44027  omabs2  44039