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 6203 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordelss 6209 | . . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | |
3 | 2 | ex 415 | . 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 ⊆ wss 3938 Ord word 6192 Oncon0 6193 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-v 3498 df-in 3945 df-ss 3954 df-uni 4841 df-tr 5175 df-po 5476 df-so 5477 df-fr 5516 df-we 5518 df-ord 6196 df-on 6197 |
This theorem is referenced by: ordunidif 6241 onelssi 6301 ssorduni 7502 suceloni 7530 tfisi 7575 tfrlem9 8023 tfrlem11 8026 oaordex 8186 oaass 8189 odi 8207 omass 8208 oewordri 8220 nnaordex 8266 domtriord 8665 hartogs 9010 card2on 9020 tskwe 9381 infxpenlem 9441 cfub 9673 cfsuc 9681 coflim 9685 hsmexlem2 9851 ondomon 9987 pwcfsdom 10007 inar1 10199 tskord 10204 grudomon 10241 gruina 10242 dfrdg2 33042 poseq 33097 sltres 33171 nosupno 33205 aomclem6 39666 iscard5 39908 |
Copyright terms: Public domain | W3C validator |