![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ordelss | Structured version Visualization version GIF version |
Description: An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.) |
Ref | Expression |
---|---|
ordelss | ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordtr 6385 | . 2 ⊢ (Ord 𝐴 → Tr 𝐴) | |
2 | trss 5277 | . . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | |
3 | 2 | imp 405 | . 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
4 | 1, 3 | sylan 578 | 1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2098 ⊆ wss 3944 Tr wtr 5266 Ord word 6370 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-v 3463 df-ss 3961 df-uni 4910 df-tr 5267 df-ord 6374 |
This theorem is referenced by: onfr 6410 onelss 6413 ordtri2or2 6470 onfununi 8362 smores3 8374 tfrlem1 8397 tfrlem9a 8407 tz7.44-2 8428 tz7.44-3 8429 oaabslem 8668 oaabs2 8670 omabslem 8671 omabs 8672 findcard3 9310 findcard3OLD 9311 nnsdomg 9327 nnsdomgOLD 9328 ordiso2 9540 ordtypelem2 9544 ordtypelem6 9548 ordtypelem7 9549 cantnf 9718 cnfcomlem 9724 ttrcltr 9741 cardmin2 10024 infxpenlem 10038 iunfictbso 10139 dfac12lem2 10169 dfac12lem3 10170 unctb 10230 ackbij2lem1 10244 ackbij1lem3 10247 ackbij1lem18 10262 ackbij2 10268 ttukeylem6 10539 ttukeylem7 10540 alephexp1 10604 fpwwe2lem7 10662 pwfseqlem3 10685 pwdjundom 10692 fz1isolem 14458 noinfbday 27699 onsuct0 36056 finxpreclem4 37004 nadd2rabtr 42955 grur1cld 43811 |
Copyright terms: Public domain | W3C validator |