MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  omsson Structured version   Visualization version   GIF version

Theorem omsson 7066
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.
StepHypRef Expression
1 dfom2 7064 . 2 ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}}
2 ssrab2 3685 . 2 {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}} ⊆ On
31, 2eqsstri 3633 1 ω ⊆ On
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  {crab 2915  wss 3572  Oncon0 5721  Lim wlim 5722  suc csuc 5723  ωcom 7062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-sbc 3434  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-tr 4751  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-we 5073  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-om 7063
This theorem is referenced by:  limomss  7067  nnon  7068  ordom  7071  omssnlim  7076  omsinds  7081  nnunifi  8208  unblem1  8209  unblem2  8210  unblem3  8211  unblem4  8212  isfinite2  8215  card2inf  8457  ackbij1lem16  9054  ackbij1lem18  9056  fin23lem26  9144  fin23lem27  9147  isf32lem5  9176  fin1a2lem6  9224  pwfseqlem3  9479  tskinf  9588  grothomex  9648  ltsopi  9707  dmaddpi  9709  dmmulpi  9710  2ndcdisj  21253  finminlem  32296
  Copyright terms: Public domain W3C validator