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

Metamath Proof Explorer

Theorem sotri3

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

Ref Expression
Hypotheses soi.1 ⊢ 𝑅 Or 𝑆
soi.2 ⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
Assertion sotri3 ( ( 𝐶 ∈ 𝑆 ∧ 𝐴 𝑅 𝐵 ∧ ¬ 𝐶 𝑅 𝐵 ) → 𝐴 𝑅 𝐶 )

Proof

Step Hyp Ref Expression
1 soi.1 ⊢ 𝑅 Or 𝑆
2 soi.2 ⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
3 2 brel ⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
4 3 simprd ⊢ ( 𝐴 𝑅 𝐵 → 𝐵 ∈ 𝑆 )
5 sotric ⊢ ( ( 𝑅 Or 𝑆 ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐶 𝑅 𝐵 ↔ ¬ ( 𝐶 = 𝐵 ∨ 𝐵 𝑅 𝐶 ) ) )
6 1 5 mpan ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐶 𝑅 𝐵 ↔ ¬ ( 𝐶 = 𝐵 ∨ 𝐵 𝑅 𝐶 ) ) )
7 6 con2bid ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ( 𝐶 = 𝐵 ∨ 𝐵 𝑅 𝐶 ) ↔ ¬ 𝐶 𝑅 𝐵 ) )
8 breq2 ⊢ ( 𝐶 = 𝐵 → ( 𝐴 𝑅 𝐶 ↔ 𝐴 𝑅 𝐵 ) )
9 8 biimprd ⊢ ( 𝐶 = 𝐵 → ( 𝐴 𝑅 𝐵 → 𝐴 𝑅 𝐶 ) )
10 1 2 sotri ⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 )
11 10 expcom ⊢ ( 𝐵 𝑅 𝐶 → ( 𝐴 𝑅 𝐵 → 𝐴 𝑅 𝐶 ) )
12 9 11 jaoi ⊢ ( ( 𝐶 = 𝐵 ∨ 𝐵 𝑅 𝐶 ) → ( 𝐴 𝑅 𝐵 → 𝐴 𝑅 𝐶 ) )
13 7 12 biimtrrdi ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ¬ 𝐶 𝑅 𝐵 → ( 𝐴 𝑅 𝐵 → 𝐴 𝑅 𝐶 ) ) )
14 13 com3r ⊢ ( 𝐴 𝑅 𝐵 → ( ( 𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( ¬ 𝐶 𝑅 𝐵 → 𝐴 𝑅 𝐶 ) ) )
15 4 14 mpan2d ⊢ ( 𝐴 𝑅 𝐵 → ( 𝐶 ∈ 𝑆 → ( ¬ 𝐶 𝑅 𝐵 → 𝐴 𝑅 𝐶 ) ) )
16 15 3imp21 ⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐴 𝑅 𝐵 ∧ ¬ 𝐶 𝑅 𝐵 ) → 𝐴 𝑅 𝐶 )