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

Metamath Proof Explorer

Theorem pltletr

Description: Transitive law for chained "less than" and "less than or equal to". ( psssstr analog.) (Contributed by NM, 2-Dec-2011)

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

Proof

Step Hyp Ref Expression
1 pltletr.b 
 |-  B = ( Base ` K )
2 pltletr.l 
 |-  .<_ = ( le ` K )
3 pltletr.s 
 |-  .< = ( lt ` K )
4 1 2 3 pleval2 
 |-  ( ( K e. Poset /\ Y e. B /\ Z e. B ) -> ( Y .<_ Z <-> ( Y .< Z \/ Y = Z ) ) )
5 4 3adant3r1 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .<_ Z <-> ( Y .< Z \/ Y = Z ) ) )
6 5 adantr 
 |-  ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( Y .<_ Z <-> ( Y .< Z \/ Y = Z ) ) )
7 1 3 plttr 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X .< Z ) )
8 7 expdimp 
 |-  ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( Y .< Z -> X .< Z ) )
9 breq2 
 |-  ( Y = Z -> ( X .< Y <-> X .< Z ) )
10 9 biimpcd 
 |-  ( X .< Y -> ( Y = Z -> X .< Z ) )
11 10 adantl 
 |-  ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( Y = Z -> X .< Z ) )
12 8 11 jaod 
 |-  ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( ( Y .< Z \/ Y = Z ) -> X .< Z ) )
13 6 12 sylbid 
 |-  ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X .< Y ) -> ( Y .<_ Z -> X .< Z ) )
14 13 expimpd 
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .<_ Z ) -> X .< Z ) )