![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sdomdomtr | Structured version Visualization version GIF version |
Description: Transitivity of strict dominance and dominance. Theorem 22(iii) of [Suppes] p. 97. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
sdomdomtr | ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sdomdom 8390 | . . 3 ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) | |
2 | domtr 8415 | . . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | |
3 | 1, 2 | sylan 580 | . 2 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
4 | simpl 483 | . . 3 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐵) | |
5 | simpr 485 | . . . . . 6 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐵 ≼ 𝐶) | |
6 | ensym 8411 | . . . . . 6 ⊢ (𝐴 ≈ 𝐶 → 𝐶 ≈ 𝐴) | |
7 | domentr 8421 | . . . . . 6 ⊢ ((𝐵 ≼ 𝐶 ∧ 𝐶 ≈ 𝐴) → 𝐵 ≼ 𝐴) | |
8 | 5, 6, 7 | syl2an 595 | . . . . 5 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) ∧ 𝐴 ≈ 𝐶) → 𝐵 ≼ 𝐴) |
9 | domnsym 8495 | . . . . 5 ⊢ (𝐵 ≼ 𝐴 → ¬ 𝐴 ≺ 𝐵) | |
10 | 8, 9 | syl 17 | . . . 4 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) ∧ 𝐴 ≈ 𝐶) → ¬ 𝐴 ≺ 𝐵) |
11 | 10 | ex 413 | . . 3 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → (𝐴 ≈ 𝐶 → ¬ 𝐴 ≺ 𝐵)) |
12 | 4, 11 | mt2d 138 | . 2 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → ¬ 𝐴 ≈ 𝐶) |
13 | brsdom 8385 | . 2 ⊢ (𝐴 ≺ 𝐶 ↔ (𝐴 ≼ 𝐶 ∧ ¬ 𝐴 ≈ 𝐶)) | |
14 | 3, 12, 13 | sylanbrc 583 | 1 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 class class class wbr 4966 ≈ cen 8359 ≼ cdom 8360 ≺ csdm 8361 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-opab 5029 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-er 8144 df-en 8363 df-dom 8364 df-sdom 8365 |
This theorem is referenced by: sdomentr 8503 sucdom 8566 infsdomnn 8630 fodomfib 8649 marypha1lem 8748 r1sdom 9054 infxpenlem 9290 infunsdom1 9486 fin56 9666 fodomb 9799 pwcfsdom 9856 cfpwsdom 9857 canthp1lem2 9926 gchpwdom 9943 gchhar 9952 gchina 9972 tsksdom 10029 tskpr 10043 tskcard 10054 gruina 10091 domalom 34242 lindsenlbs 34444 |
Copyright terms: Public domain | W3C validator |