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 
|- R Or S
soi.2 
|- R C_ ( S X. S )
Assertion sotri3 
|- ( ( C e. S /\ A R B /\ -. C R B ) -> 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 simprd 
 |-  ( A R B -> B e. S )
5 sotric 
 |-  ( ( R Or S /\ ( C e. S /\ B e. S ) ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
6 1 5 mpan 
 |-  ( ( C e. S /\ B e. S ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
7 6 con2bid 
 |-  ( ( C e. S /\ B e. S ) -> ( ( C = B \/ B R C ) <-> -. C R B ) )
8 breq2 
 |-  ( C = B -> ( A R C <-> A R B ) )
9 8 biimprd 
 |-  ( C = B -> ( A R B -> A R C ) )
10 1 2 sotri 
 |-  ( ( A R B /\ B R C ) -> A R C )
11 10 expcom 
 |-  ( B R C -> ( A R B -> A R C ) )
12 9 11 jaoi 
 |-  ( ( C = B \/ B R C ) -> ( A R B -> A R C ) )
13 7 12 biimtrrdi 
 |-  ( ( C e. S /\ B e. S ) -> ( -. C R B -> ( A R B -> A R C ) ) )
14 13 com3r 
 |-  ( A R B -> ( ( C e. S /\ B e. S ) -> ( -. C R B -> A R C ) ) )
15 4 14 mpan2d 
 |-  ( A R B -> ( C e. S -> ( -. C R B -> A R C ) ) )
16 15 3imp21 
 |-  ( ( C e. S /\ A R B /\ -. C R B ) -> A R C )