Theorem omsson 7576

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		dfom2 7574	. 2 ⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}}
2	1	ssrab3 4055	1 ⊢ ω ⊆ On

Syntax hints:  ¬ wn 3  {crab 3140   ⊆ wss 3934  Oncon0 6184  Lim wlim 6185  suc csuc 6186  ωcom 7572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320  ax-un 7453

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-om 7573

This theorem is referenced by:  limomss  7577  nnon  7578  ordom  7581  omssnlim  7586  omsinds  7592  nnunifi  8761  unblem1  8762  unblem2  8763  unblem3  8764  unblem4  8765  isfinite2  8768  card2inf  9011  ackbij1lem16  9649  ackbij1lem18  9651  fin23lem26  9739  fin23lem27  9742  isf32lem5  9771  fin1a2lem6  9819  pwfseqlem3  10074  tskinf  10183  grothomex  10243  ltsopi  10302  dmaddpi  10304  dmmulpi  10305  2ndcdisj  22056  finminlem  33659