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

Metamath Proof Explorer

Theorem poltletr

Description: Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion poltletr 
|- ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R B /\ B ( R u. _I ) C ) -> A R C ) )

Proof

Step Hyp Ref Expression
1 poleloe 
 |-  ( C e. X -> ( B ( R u. _I ) C <-> ( B R C \/ B = C ) ) )
2 1 3ad2ant3 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> ( B ( R u. _I ) C <-> ( B R C \/ B = C ) ) )
3 2 adantl 
 |-  ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B ( R u. _I ) C <-> ( B R C \/ B = C ) ) )
4 3 anbi2d 
 |-  ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R B /\ B ( R u. _I ) C ) <-> ( A R B /\ ( B R C \/ B = C ) ) ) )
5 potr 
 |-  ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R B /\ B R C ) -> A R C ) )
6 5 com12 
 |-  ( ( A R B /\ B R C ) -> ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A R C ) )
7 breq2 
 |-  ( B = C -> ( A R B <-> A R C ) )
8 7 biimpac 
 |-  ( ( A R B /\ B = C ) -> A R C )
9 8 a1d 
 |-  ( ( A R B /\ B = C ) -> ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A R C ) )
10 6 9 jaodan 
 |-  ( ( A R B /\ ( B R C \/ B = C ) ) -> ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> A R C ) )
11 10 com12 
 |-  ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R B /\ ( B R C \/ B = C ) ) -> A R C ) )
12 4 11 sylbid 
 |-  ( ( R Po X /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A R B /\ B ( R u. _I ) C ) -> A R C ) )