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 6195 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordelss 6201 | . . 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 2110 ⊆ wss 3935 Ord word 6184 Oncon0 6185 |
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 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-v 3496 df-in 3942 df-ss 3951 df-uni 4832 df-tr 5165 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-ord 6188 df-on 6189 |
This theorem is referenced by: ordunidif 6233 onelssi 6293 ssorduni 7494 suceloni 7522 tfisi 7567 tfrlem9 8015 tfrlem11 8018 oaordex 8178 oaass 8181 odi 8199 omass 8200 oewordri 8212 nnaordex 8258 domtriord 8657 hartogs 9002 card2on 9012 tskwe 9373 infxpenlem 9433 cfub 9665 cfsuc 9673 coflim 9677 hsmexlem2 9843 ondomon 9979 pwcfsdom 9999 inar1 10191 tskord 10196 grudomon 10233 gruina 10234 dfrdg2 33035 poseq 33090 sltres 33164 nosupno 33198 aomclem6 39652 iscard5 39894 |
Copyright terms: Public domain | W3C validator |