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 
|- R Or S
soi.2 
|- R C_ ( S X. S )
Assertion sotri 
|- ( ( A R B /\ B R C ) -> A R C )

Proof

Step Hyp Ref Expression
1 soi.1 
 |-  R Or S
2 soi.2 
 |-  R C_ ( S X. S )
3 2 brel 
 |-  ( A R B -> ( A e. S /\ B e. S ) )
4 3 simpld 
 |-  ( A R B -> A e. S )
5 2 brel 
 |-  ( B R C -> ( B e. S /\ C e. S ) )
6 4 5 anim12i 
 |-  ( ( A R B /\ B R C ) -> ( A e. S /\ ( B e. S /\ C e. S ) ) )
7 sotr 
 |-  ( ( R Or S /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( ( A R B /\ B R C ) -> A R C ) )
8 1 7 mpan 
 |-  ( ( A e. S /\ B e. S /\ C e. S ) -> ( ( A R B /\ B R C ) -> A R C ) )
9 8 3expb 
 |-  ( ( A e. S /\ ( B e. S /\ C e. S ) ) -> ( ( A R B /\ B R C ) -> A R C ) )
10 6 9 mpcom 
 |-  ( ( A R B /\ B R C ) -> A R C )