Theorem pltn2lp

Description: The less-than relation has no 2-cycle loops. ( pssn2lp analog.) (Contributed by NM, 2-Dec-2011)

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

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	4	ex	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\to \neg Y{\le }_{K}X\right)$$
6	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)$$
7	6	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)$$
8	5 7	nsyld	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}Y\to \neg Y\underset{\dot{}}{<}X\right)$$
9		imnan	$$⊢\left(X\underset{\dot{}}{<}Y\to \neg Y\underset{\dot{}}{<}X\right)\leftrightarrow \neg \left(X\underset{\dot{}}{<}Y\wedge Y\underset{\dot{}}{<}X\right)$$
10	8 9	sylib	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to \neg \left(X\underset{\dot{}}{<}Y\wedge Y\underset{\dot{}}{<}X\right)$$