This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvrnle

Description: The covers relation implies the negation of the converse "less than or equal to" relation. (Contributed by NM, 18-Oct-2011)

	Ref	Expression
Hypotheses	cvrle.b	$⊢ B = {Base}_{K}$
	cvrle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cvrle.c	$⊢ C = ⋖_{K}$
Assertion	cvrnle	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X C Y) \to \neg Y \underset{˙}{\leq} X$

Step	Hyp	Ref	Expression
1		cvrle.b	$⊢ B = {Base}_{K}$
2		cvrle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvrle.c	$⊢ C = ⋖_{K}$
4		eqid	$⊢ <_{K} = <_{K}$
5	1 4 3	cvrlt	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X C Y) \to X <_{K} Y$
6	1 2 4	pltnle	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X <_{K} Y) \to \neg Y \underset{˙}{\leq} X$
7	5 6	syldan	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X C Y) \to \neg Y \underset{˙}{\leq} X$