| 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 6398 | . 2 ⊢ (Ord 𝐴 → Tr 𝐴) | |
| 2 | trss 5270 | . . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | |
| 3 | 2 | imp 406 | . 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
| 4 | 1, 3 | sylan 580 | 1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ⊆ wss 3951 Tr wtr 5259 Ord word 6383 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-v 3482 df-ss 3968 df-uni 4908 df-tr 5260 df-ord 6387 |
| This theorem is referenced by: onfr 6423 onelss 6426 ordtri2or2 6483 onfununi 8381 smores3 8393 tfrlem1 8416 tfrlem9a 8426 tz7.44-2 8447 tz7.44-3 8448 oaabslem 8685 oaabs2 8687 omabslem 8688 omabs 8689 findcard3 9318 findcard3OLD 9319 nnsdomg 9335 nnsdomgOLD 9336 ordiso2 9555 ordtypelem2 9559 ordtypelem6 9563 ordtypelem7 9564 cantnf 9733 cnfcomlem 9739 ttrcltr 9756 cardmin2 10039 infxpenlem 10053 iunfictbso 10154 dfac12lem2 10185 dfac12lem3 10186 unctb 10244 ackbij2lem1 10258 ackbij1lem3 10261 ackbij1lem18 10276 ackbij2 10282 ttukeylem6 10554 ttukeylem7 10555 alephexp1 10619 fpwwe2lem7 10677 pwfseqlem3 10700 pwdjundom 10707 fz1isolem 14500 noinfbday 27765 onsuct0 36442 finxpreclem4 37395 nadd2rabtr 43397 grur1cld 44251 |
| Copyright terms: Public domain | W3C validator |