![]() |
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 6076 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordelss 6082 | . . 3 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | |
3 | 2 | ex 413 | . 2 ⊢ (Ord 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
4 | 1, 3 | syl 17 | 1 ⊢ (𝐴 ∈ On → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2081 ⊆ wss 3859 Ord word 6065 Oncon0 6066 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-v 3439 df-in 3866 df-ss 3874 df-uni 4746 df-tr 5064 df-po 5362 df-so 5363 df-fr 5402 df-we 5404 df-ord 6069 df-on 6070 |
This theorem is referenced by: ordunidif 6114 onelssi 6174 ssorduni 7356 suceloni 7384 tfisi 7429 tfrlem9 7873 tfrlem11 7876 oaordex 8034 oaass 8037 odi 8055 omass 8056 oewordri 8068 nnaordex 8114 domtriord 8510 hartogs 8854 card2on 8864 tskwe 9225 infxpenlem 9285 cfub 9517 cfsuc 9525 coflim 9529 hsmexlem2 9695 ondomon 9831 pwcfsdom 9851 inar1 10043 tskord 10048 grudomon 10085 gruina 10086 dfrdg2 32650 poseq 32705 sltres 32779 nosupno 32813 aomclem6 39163 iscard5 39405 |
Copyright terms: Public domain | W3C validator |