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

Metamath Proof Explorer

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