![]() |
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 5775 | . 2 ⊢ (Ord 𝐴 → Tr 𝐴) | |
2 | trss 4794 | . . 3 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | |
3 | 2 | imp 444 | . 2 ⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
4 | 1, 3 | sylan 487 | 1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 2030 ⊆ wss 3607 Tr wtr 4785 Ord word 5760 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-v 3233 df-in 3614 df-ss 3621 df-uni 4469 df-tr 4786 df-ord 5764 |
This theorem is referenced by: onfr 5801 onelss 5804 ordtri2or2 5861 onfununi 7483 smores3 7495 tfrlem1 7517 tfrlem9a 7527 tz7.44-2 7548 tz7.44-3 7549 oaabslem 7768 oaabs2 7770 omabslem 7771 omabs 7772 findcard3 8244 nnsdomg 8260 ordiso2 8461 ordtypelem2 8465 ordtypelem6 8469 ordtypelem7 8470 cantnf 8628 cnfcomlem 8634 cardmin2 8862 infxpenlem 8874 iunfictbso 8975 dfac12lem2 9004 dfac12lem3 9005 unctb 9065 ackbij2lem1 9079 ackbij1lem3 9082 ackbij1lem18 9097 ackbij2 9103 ttukeylem6 9374 ttukeylem7 9375 alephexp1 9439 fpwwe2lem8 9497 pwfseqlem3 9520 pwcdandom 9527 fz1isolem 13283 onsuct0 32565 finxpreclem4 33361 |
Copyright terms: Public domain | W3C validator |