ltcvrntr

Description: Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012)

	Ref	Expression
Hypotheses	ltltncvr.b	$⊢ B = {Base}_{K}$
	ltltncvr.s	$⊢ \underset{˙}{<} = <_{K}$
	ltltncvr.c	$⊢ C = ⋖_{K}$
Assertion	ltcvrntr	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Y \land Y C Z) \to \neg X C Z)$

Step	Hyp	Ref	Expression
1		ltltncvr.b	$⊢ B = {Base}_{K}$
2		ltltncvr.s	$⊢ \underset{˙}{<} = <_{K}$
3		ltltncvr.c	$⊢ C = ⋖_{K}$
4	1 2 3	cvrlt	$⊢ ((K \in A \land Y \in B \land Z \in B) \land Y C Z) \to Y \underset{˙}{<} Z$
5	4	ex	$⊢ (K \in A \land Y \in B \land Z \in B) \to (Y C Z \to Y \underset{˙}{<} Z)$
6	5	3adant3r1	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to (Y C Z \to Y \underset{˙}{<} Z)$
7	1 2 3	ltltncvr	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Y \land Y \underset{˙}{<} Z) \to \neg X C Z)$
8	6 7	sylan2d	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to ((X \underset{˙}{<} Y \land Y C Z) \to \neg X C Z)$

Metamath Proof Explorer