![]() |
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 5951 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordelss 5957 | . . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | |
3 | 2 | ex 402 | . 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2157 ⊆ wss 3769 Ord word 5940 Oncon0 5941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-v 3387 df-in 3776 df-ss 3783 df-uni 4629 df-tr 4946 df-po 5233 df-so 5234 df-fr 5271 df-we 5273 df-ord 5944 df-on 5945 |
This theorem is referenced by: ordunidif 5989 onelssi 6049 ssorduni 7219 suceloni 7247 tfisi 7292 tfrlem9 7720 tfrlem11 7723 oaordex 7878 oaass 7881 odi 7899 omass 7900 oewordri 7912 nnaordex 7958 domtriord 8348 hartogs 8691 card2on 8701 tskwe 9062 infxpenlem 9122 cfub 9359 cfsuc 9367 coflim 9371 hsmexlem2 9537 ondomon 9673 pwcfsdom 9693 inar1 9885 tskord 9890 grudomon 9927 gruina 9928 dfrdg2 32213 poseq 32266 sltres 32328 nosupno 32362 aomclem6 38414 |
Copyright terms: Public domain | W3C validator |