Theorem omsson 7854

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

Syntax hints:   → wi 4  ∀wal 1561   ⊆ wss 3907  Oncon0 6350  Lim wlim 6351  ωcom 7850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-ss 3924  df-om 7851

This theorem is referenced by:  limomss  7855  nnon  7856  ordom  7860  omssnlim  7865  omsinds  7871  nnunifi  9239  unblem1  9240  unblem2  9241  unblem3  9242  unblem4  9243  isfinite2  9246  card2inf  9505  ackbij1lem16  10205  ackbij1lem18  10207  fin23lem26  10297  fin23lem27  10300  isf32lem5  10329  fin1a2lem6  10377  pwfseqlem3  10633  tskinf  10742  grothomex  10802  ltsopi  10861  dmaddpi  10863  dmmulpi  10864  2ndcdisj  23574  finminlem  36691  ttcid  36865  dfttc2g  36879  cantnftermord  43909  omabs2  43921