Theorem omsson 7398

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

Syntax hints:  ¬ wn 3  {crab 3089   ⊆ wss 3828  Oncon0 6027  Lim wlim 6028  suc csuc 6029  ωcom 7394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pr 5184  ax-un 7277

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-sbc 3681  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-pss 3844  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-tp 4444  df-op 4446  df-uni 4711  df-br 4928  df-opab 4990  df-tr 5029  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-we 5365  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-om 7395

This theorem is referenced by:  limomss  7399  nnon  7400  ordom  7403  omssnlim  7408  omsinds  7413  nnunifi  8560  unblem1  8561  unblem2  8562  unblem3  8563  unblem4  8564  isfinite2  8567  card2inf  8810  ackbij1lem16  9451  ackbij1lem18  9453  fin23lem26  9541  fin23lem27  9544  isf32lem5  9573  fin1a2lem6  9621  pwfseqlem3  9876  tskinf  9985  grothomex  10045  ltsopi  10104  dmaddpi  10106  dmmulpi  10107  2ndcdisj  21762  finminlem  33157