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

Metamath Proof Explorer

Theorem sotri2

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 sotri2 
|- ( ( A e. S /\ -. B R A /\ 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 
 |-  ( B R C -> ( B e. S /\ C e. S ) )
4 3 simpld 
 |-  ( B R C -> B e. S )
5 sotric 
 |-  ( ( R Or S /\ ( B e. S /\ A e. S ) ) -> ( B R A <-> -. ( B = A \/ A R B ) ) )
6 1 5 mpan 
 |-  ( ( B e. S /\ A e. S ) -> ( B R A <-> -. ( B = A \/ A R B ) ) )
7 6 con2bid 
 |-  ( ( B e. S /\ A e. S ) -> ( ( B = A \/ A R B ) <-> -. B R A ) )
8 breq1 
 |-  ( B = A -> ( B R C <-> A R C ) )
9 8 biimpd 
 |-  ( B = A -> ( B R C -> A R C ) )
10 1 2 sotri 
 |-  ( ( A R B /\ B R C ) -> A R C )
11 10 ex 
 |-  ( A R B -> ( B R C -> A R C ) )
12 9 11 jaoi 
 |-  ( ( B = A \/ A R B ) -> ( B R C -> A R C ) )
13 7 12 biimtrrdi 
 |-  ( ( B e. S /\ A e. S ) -> ( -. B R A -> ( B R C -> A R C ) ) )
14 13 com3r 
 |-  ( B R C -> ( ( B e. S /\ A e. S ) -> ( -. B R A -> A R C ) ) )
15 4 14 mpand 
 |-  ( B R C -> ( A e. S -> ( -. B R A -> A R C ) ) )
16 15 3imp231 
 |-  ( ( A e. S /\ -. B R A /\ B R C ) -> A R C )