cvrle

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

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

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 A \land X \in B \land Y \in B) \land X C Y) \to X <_{K} Y$
6	2 4	pltval	$⊢ (K \in A \land X \in B \land Y \in B) \to (X <_{K} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
7	6	simprbda	$⊢ ((K \in A \land X \in B \land Y \in B) \land X <_{K} Y) \to X \underset{˙}{\leq} Y$
8	5 7	syldan	$⊢ ((K \in A \land X \in B \land Y \in B) \land X C Y) \to X \underset{˙}{\leq} Y$

Metamath Proof Explorer