![]() |
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 | dfom2 7396 | . 2 ⊢ ω = {𝑥 ∈ On ∣ suc 𝑥 ⊆ {𝑦 ∈ On ∣ ¬ Lim 𝑦}} | |
2 | 1 | ssrab3 3946 | 1 ⊢ ω ⊆ On |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 {crab 3089 ⊆ wss 3828 Oncon0 6027 Lim wlim 6028 suc csuc 6029 ωcom 7394 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2747 ax-sep 5058 ax-nul 5065 ax-pr 5184 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2756 df-cleq 2768 df-clel 2843 df-nfc 2915 df-ne 2965 df-ral 3090 df-rex 3091 df-rab 3094 df-v 3414 df-sbc 3681 df-dif 3831 df-un 3833 df-in 3835 df-ss 3842 df-pss 3844 df-nul 4178 df-if 4349 df-sn 4440 df-pr 4442 df-tp 4444 df-op 4446 df-uni 4711 df-br 4928 df-opab 4990 df-tr 5029 df-eprel 5314 df-po 5323 df-so 5324 df-fr 5363 df-we 5365 df-ord 6030 df-on 6031 df-lim 6032 df-suc 6033 df-om 7395 |
This theorem is referenced by: limomss 7399 nnon 7400 ordom 7403 omssnlim 7408 omsinds 7413 nnunifi 8560 unblem1 8561 unblem2 8562 unblem3 8563 unblem4 8564 isfinite2 8567 card2inf 8810 ackbij1lem16 9451 ackbij1lem18 9453 fin23lem26 9541 fin23lem27 9544 isf32lem5 9573 fin1a2lem6 9621 pwfseqlem3 9876 tskinf 9985 grothomex 10045 ltsopi 10104 dmaddpi 10106 dmmulpi 10107 2ndcdisj 21762 finminlem 33157 |
Copyright terms: Public domain | W3C validator |