cvrne

Description: The covers relation implies inequality. (Contributed by NM, 13-Oct-2011)

	Ref	Expression
Hypotheses	cvrne.b	$⊢ B = {Base}_{K}$
	cvrne.c	$⊢ C = ⋖_{K}$
Assertion	cvrne	$⊢ ((K \in A \land X \in B \land Y \in B) \land X C Y) \to X \neq Y$

Step	Hyp	Ref	Expression
1		cvrne.b	$⊢ B = {Base}_{K}$
2		cvrne.c	$⊢ C = ⋖_{K}$
3		eqid	$⊢ <_{K} = <_{K}$
4	1 3 2	cvrlt	$⊢ ((K \in A \land X \in B \land Y \in B) \land X C Y) \to X <_{K} Y$
5		eqid	$⊢ \leq_{K} = \leq_{K}$
6	5 3	pltval	$⊢ (K \in A \land X \in B \land Y \in B) \to (X <_{K} Y \leftrightarrow (X \leq_{K} Y \land X \neq Y))$
7	6	simplbda	$⊢ ((K \in A \land X \in B \land Y \in B) \land X <_{K} Y) \to X \neq Y$
8	4 7	syldan	$⊢ ((K \in A \land X \in B \land Y \in B) \land X C Y) \to X \neq Y$

Metamath Proof Explorer