![]() |
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 7888 | . 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | |
2 | 1 | ssrab3 4092 | 1 ⊢ ω ⊆ On |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 ⊆ wss 3963 Oncon0 6386 Lim wlim 6387 ωcom 7887 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-ss 3980 df-om 7888 |
This theorem is referenced by: limomss 7892 nnon 7893 ordom 7897 omssnlim 7902 omsinds 7908 omsindsOLD 7909 nnunifi 9325 unblem1 9326 unblem2 9327 unblem3 9328 unblem4 9329 isfinite2 9332 card2inf 9593 ackbij1lem16 10272 ackbij1lem18 10274 fin23lem26 10363 fin23lem27 10366 isf32lem5 10395 fin1a2lem6 10443 pwfseqlem3 10698 tskinf 10807 grothomex 10867 ltsopi 10926 dmaddpi 10928 dmmulpi 10929 2ndcdisj 23480 finminlem 36301 cantnftermord 43310 omabs2 43322 |
Copyright terms: Public domain | W3C validator |