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 6201 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordelss 6207 | . . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | |
3 | 2 | ex 416 | . 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2112 ⊆ wss 3853 Ord word 6190 Oncon0 6191 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-11 2160 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-v 3400 df-in 3860 df-ss 3870 df-uni 4806 df-tr 5147 df-po 5453 df-so 5454 df-fr 5494 df-we 5496 df-ord 6194 df-on 6195 |
This theorem is referenced by: ordunidif 6239 onelssi 6300 ssorduni 7541 suceloni 7570 tfisi 7615 tfrlem9 8099 tfrlem11 8102 oaordex 8264 oaass 8267 odi 8285 omass 8286 oewordri 8298 nnaordex 8344 domtriord 8770 hartogs 9138 card2on 9148 tskwe 9531 infxpenlem 9592 cfub 9828 cfsuc 9836 coflim 9840 hsmexlem2 10006 ondomon 10142 pwcfsdom 10162 inar1 10354 tskord 10359 grudomon 10396 gruina 10397 dfrdg2 33441 poseq 33482 sltres 33551 nosupno 33592 nosupbday 33594 noinfno 33607 oldssmade 33746 madebday 33766 aomclem6 40528 iscard5 40767 |
Copyright terms: Public domain | W3C validator |