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	⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐴 𝑅 𝐵 ∧ ¬ 𝐶 𝑅 𝐵 ) → 𝐴 𝑅 𝐶 )