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

Metamath Proof Explorer

Theorem plttr

Description: The less-than relation is transitive. ( psstr analog.) (Contributed by NM, 2-Dec-2011)

Ref Expression
Hypotheses pltnlt.b 
|- B = ( Base ` K )
pltnlt.s 
|- .< = ( lt ` K )
Assertion plttr 
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X .< Z ) )

Proof

Step Hyp Ref Expression
1 pltnlt.b 
 |-  B = ( Base ` K )
2 pltnlt.s 
 |-  .< = ( lt ` K )
3 eqid 
 |-  ( le ` K ) = ( le ` K )
4 3 2 pltle 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .< Y -> X ( le ` K ) Y ) )
5 4 3adant3r3 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .< Y -> X ( le ` K ) Y ) )
6 3 2 pltle 
 |-  ( ( K e. Poset /\ Y e. B /\ Z e. B ) -> ( Y .< Z -> Y ( le ` K ) Z ) )
7 6 3adant3r1 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .< Z -> Y ( le ` K ) Z ) )
8 1 3 postr 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ( le ` K ) Y /\ Y ( le ` K ) Z ) -> X ( le ` K ) Z ) )
9 5 7 8 syl2and 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X ( le ` K ) Z ) )
10 1 2 pltn2lp 
 |-  ( ( K e. Poset /\ X e. B /\ Y e. B ) -> -. ( X .< Y /\ Y .< X ) )
11 10 3adant3r3 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> -. ( X .< Y /\ Y .< X ) )
12 breq2 
 |-  ( X = Z -> ( Y .< X <-> Y .< Z ) )
13 12 anbi2d 
 |-  ( X = Z -> ( ( X .< Y /\ Y .< X ) <-> ( X .< Y /\ Y .< Z ) ) )
14 13 notbid 
 |-  ( X = Z -> ( -. ( X .< Y /\ Y .< X ) <-> -. ( X .< Y /\ Y .< Z ) ) )
15 11 14 syl5ibcom 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X = Z -> -. ( X .< Y /\ Y .< Z ) ) )
16 15 necon2ad 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X =/= Z ) )
17 9 16 jcad 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> ( X ( le ` K ) Z /\ X =/= Z ) ) )
18 3 2 pltval 
 |-  ( ( K e. Poset /\ X e. B /\ Z e. B ) -> ( X .< Z <-> ( X ( le ` K ) Z /\ X =/= Z ) ) )
19 18 3adant3r2 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .< Z <-> ( X ( le ` K ) Z /\ X =/= Z ) ) )
20 17 19 sylibrd 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X .< Z ) )