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 8645 | . . 3 ⊢ (𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵) | |
2 | domtr 8670 | . . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) | |
3 | 1, 2 | sylan 583 | . 2 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≼ 𝐶) |
4 | simpl 486 | . . 3 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐵) | |
5 | simpr 488 | . . . . . 6 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐵 ≼ 𝐶) | |
6 | ensym 8666 | . . . . . 6 ⊢ (𝐴 ≈ 𝐶 → 𝐶 ≈ 𝐴) | |
7 | domentr 8676 | . . . . . 6 ⊢ ((𝐵 ≼ 𝐶 ∧ 𝐶 ≈ 𝐴) → 𝐵 ≼ 𝐴) | |
8 | 5, 6, 7 | syl2an 599 | . . . . 5 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) ∧ 𝐴 ≈ 𝐶) → 𝐵 ≼ 𝐴) |
9 | domnsym 8761 | . . . . 5 ⊢ (𝐵 ≼ 𝐴 → ¬ 𝐴 ≺ 𝐵) | |
10 | 8, 9 | syl 17 | . . . 4 ⊢ (((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) ∧ 𝐴 ≈ 𝐶) → ¬ 𝐴 ≺ 𝐵) |
11 | 10 | ex 416 | . . 3 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → (𝐴 ≈ 𝐶 → ¬ 𝐴 ≺ 𝐵)) |
12 | 4, 11 | mt2d 138 | . 2 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → ¬ 𝐴 ≈ 𝐶) |
13 | brsdom 8640 | . 2 ⊢ (𝐴 ≺ 𝐶 ↔ (𝐴 ≼ 𝐶 ∧ ¬ 𝐴 ≈ 𝐶)) | |
14 | 3, 12, 13 | sylanbrc 586 | 1 ⊢ ((𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶) → 𝐴 ≺ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 class class class wbr 5043 ≈ cen 8612 ≼ cdom 8613 ≺ csdm 8614 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ral 3059 df-rex 3060 df-rab 3063 df-v 3403 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-op 4538 df-uni 4810 df-br 5044 df-opab 5106 df-id 5444 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-rn 5551 df-res 5552 df-ima 5553 df-fun 6371 df-fn 6372 df-f 6373 df-f1 6374 df-fo 6375 df-f1o 6376 df-er 8380 df-en 8616 df-dom 8617 df-sdom 8618 |
This theorem is referenced by: sdomentr 8769 sucdom 8864 infsdomnn 8921 fodomfib 8939 marypha1lem 9038 r1sdom 9373 infxpenlem 9610 infunsdom1 9810 fin56 9990 fodomb 10123 pwcfsdom 10180 cfpwsdom 10181 canthp1lem2 10250 gchpwdom 10267 gchhar 10276 gchina 10296 tsksdom 10353 tskpr 10367 tskcard 10378 gruina 10415 domalom 35269 lindsenlbs 35466 |
Copyright terms: Public domain | W3C validator |