cvcon3

Description: Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	cvcon3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} B \leftrightarrow ⊥ (B) ⋖_{ℋ} ⊥ (A))$

Proof

Step	Hyp	Ref	Expression
1		chpsscon3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subset B \leftrightarrow ⊥ (B) \subset ⊥ (A))$
2		chpsscon3	$⊢ (A \in C_{ℋ} \land x \in C_{ℋ}) \to (A \subset x \leftrightarrow ⊥ (x) \subset ⊥ (A))$
3	2	adantlr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to (A \subset x \leftrightarrow ⊥ (x) \subset ⊥ (A))$
4		chpsscon3	$⊢ (x \in C_{ℋ} \land B \in C_{ℋ}) \to (x \subset B \leftrightarrow ⊥ (B) \subset ⊥ (x))$
5	4	ancoms	$⊢ (B \in C_{ℋ} \land x \in C_{ℋ}) \to (x \subset B \leftrightarrow ⊥ (B) \subset ⊥ (x))$
6	5	adantll	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to (x \subset B \leftrightarrow ⊥ (B) \subset ⊥ (x))$
7	3 6	anbi12d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to ((A \subset x \land x \subset B) \leftrightarrow (⊥ (x) \subset ⊥ (A) \land ⊥ (B) \subset ⊥ (x)))$
8		choccl	$⊢ x \in C_{ℋ} \to ⊥ (x) \in C_{ℋ}$
9		psseq2	$⊢ y = ⊥ (x) \to (⊥ (B) \subset y \leftrightarrow ⊥ (B) \subset ⊥ (x))$
10		psseq1	$⊢ y = ⊥ (x) \to (y \subset ⊥ (A) \leftrightarrow ⊥ (x) \subset ⊥ (A))$
11	9 10	anbi12d	$⊢ y = ⊥ (x) \to ((⊥ (B) \subset y \land y \subset ⊥ (A)) \leftrightarrow (⊥ (B) \subset ⊥ (x) \land ⊥ (x) \subset ⊥ (A)))$
12	11	rspcev	$⊢ (⊥ (x) \in C_{ℋ} \land (⊥ (B) \subset ⊥ (x) \land ⊥ (x) \subset ⊥ (A))) \to \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A))$
13	8 12	sylan	$⊢ (x \in C_{ℋ} \land (⊥ (B) \subset ⊥ (x) \land ⊥ (x) \subset ⊥ (A))) \to \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A))$
14	13	ex	$⊢ x \in C_{ℋ} \to ((⊥ (B) \subset ⊥ (x) \land ⊥ (x) \subset ⊥ (A)) \to \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A)))$
15	14	ancomsd	$⊢ x \in C_{ℋ} \to ((⊥ (x) \subset ⊥ (A) \land ⊥ (B) \subset ⊥ (x)) \to \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A)))$
16	15	adantl	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to ((⊥ (x) \subset ⊥ (A) \land ⊥ (B) \subset ⊥ (x)) \to \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A)))$
17	7 16	sylbid	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land x \in C_{ℋ}) \to ((A \subset x \land x \subset B) \to \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A)))$
18	17	rexlimdva	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\exists x \in C_{ℋ} (A \subset x \land x \subset B) \to \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A)))$
19		chpsscon1	$⊢ (B \in C_{ℋ} \land y \in C_{ℋ}) \to (⊥ (B) \subset y \leftrightarrow ⊥ (y) \subset B)$
20	19	adantll	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (⊥ (B) \subset y \leftrightarrow ⊥ (y) \subset B)$
21		chpsscon2	$⊢ (y \in C_{ℋ} \land A \in C_{ℋ}) \to (y \subset ⊥ (A) \leftrightarrow A \subset ⊥ (y))$
22	21	ancoms	$⊢ (A \in C_{ℋ} \land y \in C_{ℋ}) \to (y \subset ⊥ (A) \leftrightarrow A \subset ⊥ (y))$
23	22	adantlr	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to (y \subset ⊥ (A) \leftrightarrow A \subset ⊥ (y))$
24	20 23	anbi12d	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((⊥ (B) \subset y \land y \subset ⊥ (A)) \leftrightarrow (⊥ (y) \subset B \land A \subset ⊥ (y)))$
25		choccl	$⊢ y \in C_{ℋ} \to ⊥ (y) \in C_{ℋ}$
26		psseq2	$⊢ x = ⊥ (y) \to (A \subset x \leftrightarrow A \subset ⊥ (y))$
27		psseq1	$⊢ x = ⊥ (y) \to (x \subset B \leftrightarrow ⊥ (y) \subset B)$
28	26 27	anbi12d	$⊢ x = ⊥ (y) \to ((A \subset x \land x \subset B) \leftrightarrow (A \subset ⊥ (y) \land ⊥ (y) \subset B))$
29	28	rspcev	$⊢ (⊥ (y) \in C_{ℋ} \land (A \subset ⊥ (y) \land ⊥ (y) \subset B)) \to \exists x \in C_{ℋ} (A \subset x \land x \subset B)$
30	25 29	sylan	$⊢ (y \in C_{ℋ} \land (A \subset ⊥ (y) \land ⊥ (y) \subset B)) \to \exists x \in C_{ℋ} (A \subset x \land x \subset B)$
31	30	ex	$⊢ y \in C_{ℋ} \to ((A \subset ⊥ (y) \land ⊥ (y) \subset B) \to \exists x \in C_{ℋ} (A \subset x \land x \subset B))$
32	31	ancomsd	$⊢ y \in C_{ℋ} \to ((⊥ (y) \subset B \land A \subset ⊥ (y)) \to \exists x \in C_{ℋ} (A \subset x \land x \subset B))$
33	32	adantl	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((⊥ (y) \subset B \land A \subset ⊥ (y)) \to \exists x \in C_{ℋ} (A \subset x \land x \subset B))$
34	24 33	sylbid	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ}) \land y \in C_{ℋ}) \to ((⊥ (B) \subset y \land y \subset ⊥ (A)) \to \exists x \in C_{ℋ} (A \subset x \land x \subset B))$
35	34	rexlimdva	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A)) \to \exists x \in C_{ℋ} (A \subset x \land x \subset B))$
36	18 35	impbid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\exists x \in C_{ℋ} (A \subset x \land x \subset B) \leftrightarrow \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A)))$
37	36	notbid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\neg \exists x \in C_{ℋ} (A \subset x \land x \subset B) \leftrightarrow \neg \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A)))$
38	1 37	anbi12d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ((A \subset B \land \neg \exists x \in C_{ℋ} (A \subset x \land x \subset B)) \leftrightarrow (⊥ (B) \subset ⊥ (A) \land \neg \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A))))$
39		cvbr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} B \leftrightarrow (A \subset B \land \neg \exists x \in C_{ℋ} (A \subset x \land x \subset B)))$
40		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
41		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
42		cvbr	$⊢ (⊥ (B) \in C_{ℋ} \land ⊥ (A) \in C_{ℋ}) \to (⊥ (B) ⋖_{ℋ} ⊥ (A) \leftrightarrow (⊥ (B) \subset ⊥ (A) \land \neg \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A))))$
43	40 41 42	syl2anr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (⊥ (B) ⋖_{ℋ} ⊥ (A) \leftrightarrow (⊥ (B) \subset ⊥ (A) \land \neg \exists y \in C_{ℋ} (⊥ (B) \subset y \land y \subset ⊥ (A))))$
44	38 39 43	3bitr4d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A ⋖_{ℋ} B \leftrightarrow ⊥ (B) ⋖_{ℋ} ⊥ (A))$

Metamath Proof Explorer

Theorem cvcon3

Proof