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 ) )