| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > sdomentr | Structured version Visualization version GIF version | ||
| Description: Transitivity of strict dominance and equinumerosity. Exercise 11 of [Suppes] p. 98. (Contributed by NM, 26-Oct-2003.) |
| Ref | Expression |
|---|---|
| sdomentr | ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≺ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | endom 8978 | . 2 ⊢ (𝐵 ≈ 𝐶 → 𝐵 ≼ 𝐶) | |
| 2 | sdomdomtr 9100 | . 2 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶) | |
| 3 | 1, 2 | sylan2 605 | 1 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≈ 𝐶) → 𝐴 ≺ 𝐶) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 class class class wbr 5112 ≈ cen 8942 ≼ cdom 8943 ≺ csdm 8944 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5260 ax-pow 5339 ax-pr 5407 ax-un 7738 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ral 3083 df-rex 3093 df-rab 3420 df-v 3460 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4876 df-br 5113 df-opab 5177 df-id 5559 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-er 8696 df-en 8946 df-dom 8947 df-sdom 8948 |
| This theorem is used by: sdomen2 9112 unxpdom2 9222 sucxpdom 9223 fofinf1o 9291 sdomsdomcardi 9968 cardsdomel 9971 cardmin2 9996 alephnbtwn2 10067 pwsdompw 10197 infdif2 10203 fin23lem27 10322 axcclem 10451 numthcor 10488 sdomsdomcard 10554 pwcfsdom 10578 cfpwsdom 10579 inawinalem 10684 inatsk 10773 r1tskina 10777 tskuni 10778 rucALT 16296 iunmbl2 25731 dirith2 27707 kardsdom 35587 erdszelem10 35704 mblfinlem1 38340 pellex 43594 rp-isfinite6 44276 harval3 44296 |
| Copyright terms: Public domain | W3C validator |