|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > omsson | Structured version Visualization version GIF version | ||
| Description: Omega is a subset of On. (Contributed by NM, 13-Jun-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) | 
| Ref | Expression | 
|---|---|
| omsson | ⊢ ω ⊆ On | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-om 7889 | . 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | |
| 2 | 1 | ssrab3 4081 | 1 ⊢ ω ⊆ On | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 ⊆ wss 3950 Oncon0 6383 Lim wlim 6384 ωcom 7888 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-ss 3967 df-om 7889 | 
| This theorem is referenced by: limomss 7893 nnon 7894 ordom 7898 omssnlim 7903 omsinds 7909 nnunifi 9328 unblem1 9329 unblem2 9330 unblem3 9331 unblem4 9332 isfinite2 9335 card2inf 9596 ackbij1lem16 10275 ackbij1lem18 10277 fin23lem26 10366 fin23lem27 10369 isf32lem5 10398 fin1a2lem6 10446 pwfseqlem3 10701 tskinf 10810 grothomex 10870 ltsopi 10929 dmaddpi 10931 dmmulpi 10932 2ndcdisj 23465 finminlem 36320 cantnftermord 43338 omabs2 43350 | 
| Copyright terms: Public domain | W3C validator |