pltnle

Description: "Less than" implies not converse "less than or equal to". (Contributed by NM, 18-Oct-2011)

	Ref	Expression
Hypotheses	pleval2.b	$⊢ B = {Base}_{K}$
	pleval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pleval2.s	$⊢ \underset{˙}{<} = <_{K}$
Assertion	pltnle	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \neg Y \underset{˙}{\leq} X$

Step	Hyp	Ref	Expression
1		pleval2.b	$⊢ B = {Base}_{K}$
2		pleval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		pleval2.s	$⊢ \underset{˙}{<} = <_{K}$
4	2 3	pltval	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
5	1 2	posasymb	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \leftrightarrow X = Y)$
6	5	biimpd	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} X) \to X = Y)$
7	6	expdimp	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (Y \underset{˙}{\leq} X \to X = Y)$
8	7	necon3ad	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{\leq} Y) \to (X \neq Y \to \neg Y \underset{˙}{\leq} X)$
9	8	expimpd	$⊢ (K \in Poset \land X \in B \land Y \in B) \to ((X \underset{˙}{\leq} Y \land X \neq Y) \to \neg Y \underset{˙}{\leq} X)$
10	4 9	sylbid	$⊢ (K \in Poset \land X \in B \land Y \in B) \to (X \underset{˙}{<} Y \to \neg Y \underset{˙}{\leq} X)$
11	10	imp	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to \neg Y \underset{˙}{\leq} X$

Metamath Proof Explorer