pltnlt

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

	Ref	Expression
Hypotheses	pltnlt.b	$⊢ B = {Base}_{K}$
	pltnlt.s	$⊢ \underset{˙}{<} = <_{K}$
Assertion	pltnlt	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \neg 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	3 2	pltle	$⊢ (K \in Poset \land Y \in B \land X \in B) \to (Y \underset{˙}{<} X \to Y \leq_{K} X)$
6	5	3com23	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (Y \underset{˙}{<} X \to Y \leq_{K} X)$
7	6	adantr	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to (Y \underset{˙}{<} X \to Y \leq_{K} X)$
8	4 7	mtod	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \neg Y \underset{˙}{<} X$

Metamath Proof Explorer