![]() |
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 6396 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordelss 6402 | . . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | |
3 | 2 | ex 412 | . 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ⊆ wss 3963 Ord word 6385 Oncon0 6386 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-v 3480 df-ss 3980 df-uni 4913 df-tr 5266 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-ord 6389 df-on 6390 |
This theorem is referenced by: ordunidif 6435 onelssi 6501 ssorduni 7798 sucexeloniOLD 7830 suceloniOLD 7832 tfisi 7880 poseq 8182 tfrlem9 8424 tfrlem11 8427 oaordex 8595 oaass 8598 odi 8616 omass 8617 oewordri 8629 nnaordex 8675 domtriord 9162 hartogs 9582 card2on 9592 tskwe 9988 infxpenlem 10051 cfub 10287 cfsuc 10295 coflim 10299 hsmexlem2 10465 ondomon 10601 pwcfsdom 10621 inar1 10813 tskord 10818 grudomon 10855 gruina 10856 sltres 27722 nosupno 27763 nosupbday 27765 noinfno 27778 oldssmade 27931 madebday 27953 mulsproplem13 28169 mulsproplem14 28170 dfrdg2 35777 aomclem6 43048 nnoeomeqom 43302 naddgeoa 43384 naddwordnexlem1 43387 naddwordnexlem4 43391 iscard5 43526 |
Copyright terms: Public domain | W3C validator |