Theorem pltle

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

	Ref	Expression
Hypotheses	pltval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	pltval.s	$$⊢\underset{\dot{}}{<}={<}_K$$
Assertion	pltle	$$⊢\left(K\in A\wedge X\in B\wedge Y\in C\right)\to \left(X\underset{\dot{}}{<}Y\to X\underset{\dot{}}{\le }Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		pltval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		pltval.s	$$⊢\underset{\dot{}}{<}={<}_K$$
3	1 2	pltval	$$⊢\left(K\in A\wedge X\in B\wedge Y\in C\right)\to \left(X\underset{\dot{}}{<}Y\leftrightarrow \left(X\underset{\dot{}}{\le }Y\wedge X\ne Y\right)\right)$$
4	3	simprbda	$$⊢\left(\left(K\in A\wedge X\in B\wedge Y\in C\right)\wedge X\underset{\dot{}}{<}Y\right)\to X\underset{\dot{}}{\le }Y$$
5	4	ex	$$⊢\left(K\in A\wedge X\in B\wedge Y\in C\right)\to \left(X\underset{\dot{}}{<}Y\to X\underset{\dot{}}{\le }Y\right)$$