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 = {Base}_{K}$
	pltnlt.s	$⊢ \underset{˙}{<} = <_{K}$
Assertion	pltn2lp	$⊢ (K \in Poset \land X \in B \land Y \in B) \to \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} X)$

Step	Hyp	Ref	Expression
1		pltnlt.b	$⊢ B = {Base}_{K}$
2		pltnlt.s	$⊢ \underset{˙}{<} = <_{K}$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4	1 3 2	pltnle	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \neg Y \leq_{K} X$
5	4	ex	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to \neg Y \leq_{K} X)$
6	3 2	pltle	$⊢ (K \in Poset \land Y \in B \land X \in B) \to (Y \underset{˙}{<} X \to Y \leq_{K} X)$
7	6	3com23	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (Y \underset{˙}{<} X \to Y \leq_{K} X)$
8	5 7	nsyld	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to \neg Y \underset{˙}{<} X)$
9		imnan	$⊢ (X \underset{˙}{<} Y \to \neg Y \underset{˙}{<} X) \leftrightarrow \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} X)$
10	8 9	sylib	$⊢ (K \in Poset \land X \in B \land Y \in B) \to \neg (X \underset{˙}{<} Y \land Y \underset{˙}{<} X)$

Metamath Proof Explorer