cvrletrN

Description: Property of an element above a covering. (Contributed by NM, 7-Dec-2012) (New usage is discouraged.)

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

Step	Hyp	Ref	Expression
1		cvrletr.b	$⊢ B = {Base}_{K}$
2		cvrletr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvrletr.s	$⊢ \underset{˙}{<} = <_{K}$
4		cvrletr.c	$⊢ C = ⋖_{K}$
5		simpll	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X C Y) \to K \in Poset$
6		simplr1	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X C Y) \to X \in B$
7		simplr2	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X C Y) \to Y \in B$
8		simpr	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X C Y) \to X C Y$
9	1 3 4	cvrlt	$⊢ ((K \in Poset \land X \in B \land Y \in B) \land X C Y) \to X \underset{˙}{<} Y$
10	5 6 7 8 9	syl31anc	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X C Y) \to X \underset{˙}{<} Y$
11	1 2 3	pltletr	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Y \land Y \underset{˙}{\leq} Z) \to X \underset{˙}{<} Z)$
12	11	adantr	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X C Y) \to ((X \underset{˙}{<} Y \land Y \underset{˙}{\leq} Z) \to X \underset{˙}{<} Z)$
13	10 12	mpand	$⊢ ((K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \land X C Y) \to (Y \underset{˙}{\leq} Z \to X \underset{˙}{<} Z)$
14	13	expimpd	$⊢ (K \in Poset \land (X \in B \land Y \in B \land Z \in B)) \to ((X C Y \land Y \underset{˙}{\leq} Z) \to X \underset{˙}{<} Z)$

Metamath Proof Explorer