Metamath Proof Explorer


Theorem pltle

Description: "Less than" implies "less than or equal to". ( pssss analog.) (Contributed by NM, 4-Dec-2011)

Ref Expression
Hypotheses pltval.l
|- .<_ = ( le ` K )
pltval.s
|- .< = ( lt ` K )
Assertion pltle
|- ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y -> X .<_ Y ) )

Proof

Step Hyp Ref Expression
1 pltval.l
 |-  .<_ = ( le ` K )
2 pltval.s
 |-  .< = ( lt ` K )
3 1 2 pltval
 |-  ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y <-> ( X .<_ Y /\ X =/= Y ) ) )
4 3 simprbda
 |-  ( ( ( K e. A /\ X e. B /\ Y e. C ) /\ X .< Y ) -> X .<_ Y )
5 4 ex
 |-  ( ( K e. A /\ X e. B /\ Y e. C ) -> ( X .< Y -> X .<_ Y ) )