cvnsym

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

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

Step	Hyp	Ref	Expression
1		cvpss	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} B \to A \subset B)$
2		cvpss	$⊢ (B \in C_{ℋ} \land A \in C_{ℋ}) \to (B ⋖_{ℋ} A \to B \subset A)$
3	2	ancoms	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (B ⋖_{ℋ} A \to B \subset A)$
4		pssn2lp	$⊢ \neg (B \subset A \land A \subset B)$
5	4	imnani	$⊢ B \subset A \to \neg A \subset B$
6	3 5	syl6	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (B ⋖_{ℋ} A \to \neg A \subset B)$
7	6	con2d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subset B \to \neg B ⋖_{ℋ} A)$
8	1 7	syld	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} B \to \neg B ⋖_{ℋ} A)$

Metamath Proof Explorer