![]() |
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 7860 | . 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | |
2 | 1 | ssrab3 4081 | 1 ⊢ ω ⊆ On |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1537 ⊆ wss 3949 Oncon0 6365 Lim wlim 6366 ωcom 7859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-rab 3431 df-v 3474 df-in 3956 df-ss 3966 df-om 7860 |
This theorem is referenced by: limomss 7864 nnon 7865 ordom 7869 omssnlim 7874 omsinds 7880 omsindsOLD 7881 nnunifi 9298 unblem1 9299 unblem2 9300 unblem3 9301 unblem4 9302 isfinite2 9305 card2inf 9554 ackbij1lem16 10234 ackbij1lem18 10236 fin23lem26 10324 fin23lem27 10327 isf32lem5 10356 fin1a2lem6 10404 pwfseqlem3 10659 tskinf 10768 grothomex 10828 ltsopi 10887 dmaddpi 10889 dmmulpi 10890 2ndcdisj 23182 finminlem 35508 cantnftermord 42374 omabs2 42386 |
Copyright terms: Public domain | W3C validator |