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 6198 | . 2 ⊢ (Ord 𝐴 → Tr 𝐴) | |
2 | trss 5172 | . . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | |
3 | 2 | imp 407 | . 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
4 | 1, 3 | sylan 580 | 1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 ⊆ wss 3933 Tr wtr 5163 Ord word 6183 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-v 3494 df-in 3940 df-ss 3949 df-uni 4831 df-tr 5164 df-ord 6187 |
This theorem is referenced by: onfr 6223 onelss 6226 ordtri2or2 6280 onfununi 7967 smores3 7979 tfrlem1 8001 tfrlem9a 8011 tz7.44-2 8032 tz7.44-3 8033 oaabslem 8259 oaabs2 8261 omabslem 8262 omabs 8263 findcard3 8749 nnsdomg 8765 ordiso2 8967 ordtypelem2 8971 ordtypelem6 8975 ordtypelem7 8976 cantnf 9144 cnfcomlem 9150 cardmin2 9415 infxpenlem 9427 iunfictbso 9528 dfac12lem2 9558 dfac12lem3 9559 unctb 9615 ackbij2lem1 9629 ackbij1lem3 9632 ackbij1lem18 9647 ackbij2 9653 ttukeylem6 9924 ttukeylem7 9925 alephexp1 9989 fpwwe2lem8 10047 pwfseqlem3 10070 pwdjundom 10077 fz1isolem 13807 onsuct0 33686 finxpreclem4 34557 grur1cld 40445 |
Copyright terms: Public domain | W3C validator |