Metamath Proof Explorer


Theorem plelttr

Description: Transitive law for chained "less than or equal to" and "less than". ( sspsstr analog.) (Contributed by NM, 2-May-2012)

Ref Expression
Hypotheses pltletr.b
|- B = ( Base ` K )
pltletr.l
|- .<_ = ( le ` K )
pltletr.s
|- .< = ( lt ` K )
Assertion plelttr
|- ( ( 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 /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X .< Y \/ X = Y ) ) )
5 4 3adant3r3
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y <-> ( X .< Y \/ X = Y ) ) )
6 1 3 plttr
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X .< Z ) )
7 6 expd
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .< Y -> ( Y .< Z -> X .< Z ) ) )
8 breq1
 |-  ( X = Y -> ( X .< Z <-> Y .< Z ) )
9 8 biimprd
 |-  ( X = Y -> ( Y .< Z -> X .< Z ) )
10 9 a1i
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X = Y -> ( Y .< Z -> X .< Z ) ) )
11 7 10 jaod
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y \/ X = Y ) -> ( Y .< Z -> X .< Z ) ) )
12 5 11 sylbid
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y -> ( Y .< Z -> X .< Z ) ) )
13 12 impd
 |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .< Z ) -> X .< Z ) )