![]() |
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 6400 | . 2 ⊢ (Ord 𝐴 → Tr 𝐴) | |
2 | trss 5276 | . . 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 2106 ⊆ wss 3963 Tr wtr 5265 Ord word 6385 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-v 3480 df-ss 3980 df-uni 4913 df-tr 5266 df-ord 6389 |
This theorem is referenced by: onfr 6425 onelss 6428 ordtri2or2 6485 onfununi 8380 smores3 8392 tfrlem1 8415 tfrlem9a 8425 tz7.44-2 8446 tz7.44-3 8447 oaabslem 8684 oaabs2 8686 omabslem 8687 omabs 8688 findcard3 9316 findcard3OLD 9317 nnsdomg 9333 nnsdomgOLD 9334 ordiso2 9553 ordtypelem2 9557 ordtypelem6 9561 ordtypelem7 9562 cantnf 9731 cnfcomlem 9737 ttrcltr 9754 cardmin2 10037 infxpenlem 10051 iunfictbso 10152 dfac12lem2 10183 dfac12lem3 10184 unctb 10242 ackbij2lem1 10256 ackbij1lem3 10259 ackbij1lem18 10274 ackbij2 10280 ttukeylem6 10552 ttukeylem7 10553 alephexp1 10617 fpwwe2lem7 10675 pwfseqlem3 10698 pwdjundom 10705 fz1isolem 14497 noinfbday 27780 onsuct0 36424 finxpreclem4 37377 nadd2rabtr 43374 grur1cld 44228 |
Copyright terms: Public domain | W3C validator |