Theorem pltirr

Description: The "less than" relation is not reflexive. ( pssirr analog.) (Contributed by NM, 7-Feb-2012)

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

Proof

Step	Hyp	Ref	Expression
1		pltne.s	$$⊢\underset{\dot{}}{<}={<}_K$$
2		eqid	$$⊢X=X$$
3	1	pltne	$$⊢\left(K\in A\wedge X\in B\wedge X\in B\right)\to \left(X\underset{\dot{}}{<}X\to X\ne X\right)$$
4	3	3anidm23	$$⊢\left(K\in A\wedge X\in B\right)\to \left(X\underset{\dot{}}{<}X\to X\ne X\right)$$
5	4	necon2bd	$$⊢\left(K\in A\wedge X\in B\right)\to \left(X=X\to \neg X\underset{\dot{}}{<}X\right)$$
6	2 5	mpi	$$⊢\left(K\in A\wedge X\in B\right)\to \neg X\underset{\dot{}}{<}X$$