Theorem omsson 7691

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

Syntax hints:   → wi 4  ∀wal 1537   ⊆ wss 3883  Oncon0 6251  Lim wlim 6252  ωcom 7687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-om 7688

This theorem is referenced by:  limomss  7692  nnon  7693  ordom  7697  omssnlim  7702  omsinds  7708  omsindsOLD  7709  nnunifi  8995  unblem1  8996  unblem2  8997  unblem3  8998  unblem4  8999  isfinite2  9002  card2inf  9244  ackbij1lem16  9922  ackbij1lem18  9924  fin23lem26  10012  fin23lem27  10015  isf32lem5  10044  fin1a2lem6  10092  pwfseqlem3  10347  tskinf  10456  grothomex  10516  ltsopi  10575  dmaddpi  10577  dmmulpi  10578  2ndcdisj  22515  finminlem  34434