cvrntr

Description: The covers relation is not transitive. ( cvntr analog.) (Contributed by NM, 18-Jun-2012)

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

Step	Hyp	Ref	Expression
1		cvrntr.b	$⊢ B = {Base}_{K}$
2		cvrntr.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	4	ex	$⊢ (K \in A \land X \in B \land Y \in B) \to (X C Y \to X <_{K} Y)$
6	5	3adant3r3	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to (X C Y \to X <_{K} Y)$
7	1 3 2	ltcvrntr	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to ((X <_{K} Y \land Y C Z) \to \neg X C Z)$
8	6 7	syland	$⊢ (K \in A \land (X \in B \land Y \in B \land Z \in B)) \to ((X C Y \land Y C Z) \to \neg X C Z)$

Metamath Proof Explorer