![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > onss | Structured version Visualization version GIF version |
Description: An ordinal number is a subset of the class of ordinal numbers. (Contributed by NM, 5-Jun-1994.) |
Ref | Expression |
---|---|
onss | ⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni 5986 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordsson 7267 | . 2 ⊢ (Ord 𝐴 → 𝐴 ⊆ On) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ⊆ wss 3792 Ord word 5975 Oncon0 5976 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pr 5138 ax-un 7226 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-pss 3808 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-tr 4988 df-eprel 5266 df-po 5274 df-so 5275 df-fr 5314 df-we 5316 df-ord 5979 df-on 5980 |
This theorem is referenced by: predon 7269 onuni 7271 onminex 7285 suceloni 7291 onssi 7315 tfi 7331 tfr3 7778 tz7.49 7823 tz7.49c 7824 oacomf1olem 7928 oeeulem 7965 ordtypelem2 8713 cantnfcl 8861 cantnflt 8866 cantnfp1lem3 8874 oemapvali 8878 cantnflem1c 8881 cantnflem1d 8882 cantnflem1 8883 cantnf 8887 cnfcom 8894 cnfcom3lem 8897 infxpenlem 9169 ac10ct 9190 dfac12lem1 9300 dfac12lem2 9301 cfeq0 9413 cfsuc 9414 cff1 9415 cfflb 9416 cofsmo 9426 cfsmolem 9427 alephsing 9433 zorn2lem2 9654 ttukeylem3 9668 ttukeylem5 9670 ttukeylem6 9671 inar1 9932 soseq 32343 nosupno 32438 ontgval 33013 aomclem6 38588 |
Copyright terms: Public domain | W3C validator |