![]() |
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 7876 | . 2 ⊢ ω = {𝑥 ∈ On ∣ ∀𝑦(Lim 𝑦 → 𝑥 ∈ 𝑦)} | |
2 | 1 | ssrab3 4078 | 1 ⊢ ω ⊆ On |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 ⊆ wss 3946 Oncon0 6375 Lim wlim 6376 ωcom 7875 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-ss 3963 df-om 7876 |
This theorem is referenced by: limomss 7880 nnon 7881 ordom 7885 omssnlim 7890 omsinds 7896 omsindsOLD 7897 nnunifi 9331 unblem1 9332 unblem2 9333 unblem3 9334 unblem4 9335 isfinite2 9338 card2inf 9594 ackbij1lem16 10274 ackbij1lem18 10276 fin23lem26 10364 fin23lem27 10367 isf32lem5 10396 fin1a2lem6 10444 pwfseqlem3 10699 tskinf 10808 grothomex 10868 ltsopi 10927 dmaddpi 10929 dmmulpi 10930 2ndcdisj 23443 finminlem 35978 cantnftermord 42923 omabs2 42935 |
Copyright terms: Public domain | W3C validator |