![]() |
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 5990 | . 2 ⊢ (Ord 𝐴 → Tr 𝐴) | |
2 | trss 4996 | . . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | |
3 | 2 | imp 397 | . 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
4 | 1, 3 | sylan 575 | 1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∈ wcel 2107 ⊆ wss 3792 Tr wtr 4987 Ord word 5975 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-v 3400 df-in 3799 df-ss 3806 df-uni 4672 df-tr 4988 df-ord 5979 |
This theorem is referenced by: onfr 6015 onelss 6018 ordtri2or2 6072 onfununi 7721 smores3 7733 tfrlem1 7755 tfrlem9a 7765 tz7.44-2 7786 tz7.44-3 7787 oaabslem 8007 oaabs2 8009 omabslem 8010 omabs 8011 findcard3 8491 nnsdomg 8507 ordiso2 8709 ordtypelem2 8713 ordtypelem6 8717 ordtypelem7 8718 cantnf 8887 cnfcomlem 8893 cardmin2 9157 infxpenlem 9169 iunfictbso 9270 dfac12lem2 9301 dfac12lem3 9302 unctb 9362 ackbij2lem1 9376 ackbij1lem3 9379 ackbij1lem18 9394 ackbij2 9400 ttukeylem6 9671 ttukeylem7 9672 alephexp1 9736 fpwwe2lem8 9794 pwfseqlem3 9817 pwcdandom 9824 fz1isolem 13559 onsuct0 33023 finxpreclem4 33826 |
Copyright terms: Public domain | W3C validator |