This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sotr2

Description: A transitivity relation. (Read B <_ C and C < D implies B < D .) (Contributed by Mario Carneiro, 10-May-2013)

Ref Expression
Assertion sotr2 ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ¬ 𝐶 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) → 𝐵 𝑅 𝐷 ) )

Proof

Step Hyp Ref Expression
1 sotric ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐶 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴 ) ) → ( 𝐶 𝑅 𝐵 ↔ ¬ ( 𝐶 = 𝐵 ∨ 𝐵 𝑅 𝐶 ) ) )
2 1 ancom2s ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐶 𝑅 𝐵 ↔ ¬ ( 𝐶 = 𝐵 ∨ 𝐵 𝑅 𝐶 ) ) )
3 2 3adantr3 ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 𝑅 𝐵 ↔ ¬ ( 𝐶 = 𝐵 ∨ 𝐵 𝑅 𝐶 ) ) )
4 3 con2bid ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐶 = 𝐵 ∨ 𝐵 𝑅 𝐶 ) ↔ ¬ 𝐶 𝑅 𝐵 ) )
5 breq1 ⊢ ( 𝐶 = 𝐵 → ( 𝐶 𝑅 𝐷 ↔ 𝐵 𝑅 𝐷 ) )
6 5 biimpd ⊢ ( 𝐶 = 𝐵 → ( 𝐶 𝑅 𝐷 → 𝐵 𝑅 𝐷 ) )
7 6 a1i ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐶 = 𝐵 → ( 𝐶 𝑅 𝐷 → 𝐵 𝑅 𝐷 ) ) )
8 sotr ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) → 𝐵 𝑅 𝐷 ) )
9 8 expd ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( 𝐵 𝑅 𝐶 → ( 𝐶 𝑅 𝐷 → 𝐵 𝑅 𝐷 ) ) )
10 7 9 jaod ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐶 = 𝐵 ∨ 𝐵 𝑅 𝐶 ) → ( 𝐶 𝑅 𝐷 → 𝐵 𝑅 𝐷 ) ) )
11 4 10 sylbird ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ¬ 𝐶 𝑅 𝐵 → ( 𝐶 𝑅 𝐷 → 𝐵 𝑅 𝐷 ) ) )
12 11 impd ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ¬ 𝐶 𝑅 𝐵 ∧ 𝐶 𝑅 𝐷 ) → 𝐵 𝑅 𝐷 ) )