Theorem pltne

Description: The "less than" relation is not reflexive. ( df-pss analog.) (Contributed by NM, 2-Dec-2011)

	Ref	Expression
Hypothesis	pltne.s	$$⊢\underset{\dot{}}{<}={<}_K$$
Assertion	pltne	$$⊢\left(K\in A\wedge X\in B\wedge Y\in C\right)\to \left(X\underset{\dot{}}{<}Y\to X\ne Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		pltne.s	$$⊢\underset{\dot{}}{<}={<}_K$$
2		eqid	$$⊢{\le }_K={\le }_K$$
3	2 1	pltval	$$⊢\left(K\in A\wedge X\in B\wedge Y\in C\right)\to \left(X\underset{\dot{}}{<}Y\leftrightarrow \left(X{\le }_{K}Y\wedge X\ne Y\right)\right)$$
4	3	simplbda	$$⊢\left(\left(K\in A\wedge X\in B\wedge Y\in C\right)\wedge X\underset{\dot{}}{<}Y\right)\to X\ne 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\ne Y\right)$$