cvntr

Description: The covers relation is not transitive. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	cvntr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ((A ⋖_{ℋ} B \land B ⋖_{ℋ} C) \to \neg A ⋖_{ℋ} C)$

Step	Hyp	Ref	Expression
1		cvpss	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} B \to A \subset B)$
2	1	3adant3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (A ⋖_{ℋ} B \to A \subset B)$
3		cvpss	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to (B ⋖_{ℋ} C \to B \subset C)$
4	3	3adant1	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (B ⋖_{ℋ} C \to B \subset C)$
5		cvnbtwn	$⊢ (A \in C_{ℋ} \land C \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} C \to \neg (A \subset B \land B \subset C))$
6	5	3com23	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to (A ⋖_{ℋ} C \to \neg (A \subset B \land B \subset C))$
7	6	con2d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ((A \subset B \land B \subset C) \to \neg A ⋖_{ℋ} C)$
8	2 4 7	syl2and	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land C \in C_{ℋ}) \to ((A ⋖_{ℋ} B \land B ⋖_{ℋ} C) \to \neg A ⋖_{ℋ} C)$

Metamath Proof Explorer