Theorem pltnlt

Description: The less-than relation implies the negation of its inverse. (Contributed by NM, 18-Oct-2011)

	Ref	Expression
Hypotheses	pltnlt.b	$$⊢B={\mathrm{Base}}_K$$
	pltnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
Assertion	pltnlt	$$⊢\left(\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{<}Y\right)\to \neg Y\underset{\dot{}}{<}X$$

Proof

Step	Hyp	Ref	Expression
1		pltnlt.b	$$⊢B={\mathrm{Base}}_K$$
2		pltnlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
3		eqid	$$⊢{\le }_K={\le }_K$$
4	1 3 2	pltnle	$$⊢\left(\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{<}Y\right)\to \neg Y{\le }_{K}X$$
5	3 2	pltle	$$⊢\left(K\in \mathrm{Poset}\wedge Y\in B\wedge X\in B\right)\to \left(Y\underset{\dot{}}{<}X\to Y{\le }_{K}X\right)$$
6	5	3com23	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to \left(Y\underset{\dot{}}{<}X\to Y{\le }_{K}X\right)$$
7	6	adantr	$$⊢\left(\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{<}Y\right)\to \left(Y\underset{\dot{}}{<}X\to Y{\le }_{K}X\right)$$
8	4 7	mtod	$$⊢\left(\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\wedge X\underset{\dot{}}{<}Y\right)\to \neg Y\underset{\dot{}}{<}X$$