![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > onelss | Structured version Visualization version GIF version |
Description: An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
onelss | ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni 6381 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordelss 6387 | . . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | |
3 | 2 | ex 411 | . 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 ⊆ wss 3944 Ord word 6370 Oncon0 6371 |
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-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-v 3463 df-ss 3961 df-uni 4910 df-tr 5267 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-ord 6374 df-on 6375 |
This theorem is referenced by: ordunidif 6420 onelssi 6486 ssorduni 7782 sucexeloniOLD 7814 suceloniOLD 7816 tfisi 7864 poseq 8163 tfrlem9 8406 tfrlem11 8409 oaordex 8579 oaass 8582 odi 8600 omass 8601 oewordri 8613 nnaordex 8659 domtriord 9148 hartogs 9569 card2on 9579 tskwe 9975 infxpenlem 10038 cfub 10274 cfsuc 10282 coflim 10286 hsmexlem2 10452 ondomon 10588 pwcfsdom 10608 inar1 10800 tskord 10805 grudomon 10842 gruina 10843 sltres 27641 nosupno 27682 nosupbday 27684 noinfno 27697 oldssmade 27850 madebday 27872 mulsproplem13 28078 mulsproplem14 28079 dfrdg2 35522 aomclem6 42625 nnoeomeqom 42883 naddgeoa 42966 naddwordnexlem1 42969 naddwordnexlem4 42973 iscard5 43108 |
Copyright terms: Public domain | W3C validator |