Theorem sotri

Description: A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996) (Revised by Mario Carneiro, 10-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		soi.1	⊢ 𝑅 Or 𝑆
2		soi.2	⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
3	2	brel	⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) )
4	3	simpld	⊢ ( 𝐴 𝑅 𝐵 → 𝐴 ∈ 𝑆 )
5	2	brel	⊢ ( 𝐵 𝑅 𝐶 → ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) )
6	4 5	anim12i	⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → ( 𝐴 ∈ 𝑆 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) )
7		sotr	⊢ ( ( 𝑅 Or 𝑆 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
8	1 7	mpan	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
9	8	3expb	⊢ ( ( 𝐴 ∈ 𝑆 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
10	6 9	mpcom	⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 )