cvexchlem

Description: Lemma for cvexchi . (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	chpssat.1	$⊢ A \in C_{ℋ}$
	chpssat.2	$⊢ B \in C_{ℋ}$
Assertion	cvexchlem	$⊢ (A \cap B) ⋖_{ℋ} B \to A ⋖_{ℋ} (A \lor_{ℋ} B)$

Proof

Step	Hyp	Ref	Expression
1		chpssat.1	$⊢ A \in C_{ℋ}$
2		chpssat.2	$⊢ B \in C_{ℋ}$
3	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
4		cvpss	$⊢ (A \cap B \in C_{ℋ} \land B \in C_{ℋ}) \to ((A \cap B) ⋖_{ℋ} B \to A \cap B \subset B)$
5	3 2 4	mp2an	$⊢ (A \cap B) ⋖_{ℋ} B \to A \cap B \subset B$
6	3 2	chpssati	$⊢ A \cap B \subset B \to \exists x \in HAtoms (x \subseteq B \land \neg x \subseteq A \cap B)$
7	5 6	syl	$⊢ (A \cap B) ⋖_{ℋ} B \to \exists x \in HAtoms (x \subseteq B \land \neg x \subseteq A \cap B)$
8		ssin	$⊢ (x \subseteq A \land x \subseteq B) \leftrightarrow x \subseteq A \cap B$
9		ancom	$⊢ (x \subseteq A \land x \subseteq B) \leftrightarrow (x \subseteq B \land x \subseteq A)$
10	8 9	bitr3i	$⊢ x \subseteq A \cap B \leftrightarrow (x \subseteq B \land x \subseteq A)$
11	10	baibr	$⊢ x \subseteq B \to (x \subseteq A \leftrightarrow x \subseteq A \cap B)$
12	11	notbid	$⊢ x \subseteq B \to (\neg x \subseteq A \leftrightarrow \neg x \subseteq A \cap B)$
13	12	biimpar	$⊢ (x \subseteq B \land \neg x \subseteq A \cap B) \to \neg x \subseteq A$
14		chcv1	$⊢ (A \in C_{ℋ} \land x \in HAtoms) \to (\neg x \subseteq A \leftrightarrow A ⋖_{ℋ} (A \lor_{ℋ} x))$
15	1 14	mpan	$⊢ x \in HAtoms \to (\neg x \subseteq A \leftrightarrow A ⋖_{ℋ} (A \lor_{ℋ} x))$
16	15	biimpa	$⊢ (x \in HAtoms \land \neg x \subseteq A) \to A ⋖_{ℋ} (A \lor_{ℋ} x)$
17	13 16	sylan2	$⊢ (x \in HAtoms \land (x \subseteq B \land \neg x \subseteq A \cap B)) \to A ⋖_{ℋ} (A \lor_{ℋ} x)$
18	17	adantrr	$⊢ (x \in HAtoms \land ((x \subseteq B \land \neg x \subseteq A \cap B) \land (A \cap B) ⋖_{ℋ} B)) \to A ⋖_{ℋ} (A \lor_{ℋ} x)$
19		atelch	$⊢ x \in HAtoms \to x \in C_{ℋ}$
20	1 2	chabs1i	$⊢ A \lor_{ℋ} (A \cap B) = A$
21	20	oveq1i	$⊢ (A \lor_{ℋ} (A \cap B)) \lor_{ℋ} x = A \lor_{ℋ} x$
22		chjass	$⊢ (A \in C_{ℋ} \land A \cap B \in C_{ℋ} \land x \in C_{ℋ}) \to (A \lor_{ℋ} (A \cap B)) \lor_{ℋ} x = A \lor_{ℋ} ((A \cap B) \lor_{ℋ} x)$
23	1 3 22	mp3an12	$⊢ x \in C_{ℋ} \to (A \lor_{ℋ} (A \cap B)) \lor_{ℋ} x = A \lor_{ℋ} ((A \cap B) \lor_{ℋ} x)$
24	21 23	syl5reqr	$⊢ x \in C_{ℋ} \to A \lor_{ℋ} ((A \cap B) \lor_{ℋ} x) = A \lor_{ℋ} x$
25	24	adantr	$⊢ (x \in C_{ℋ} \land ((x \subseteq B \land \neg x \subseteq A \cap B) \land (A \cap B) ⋖_{ℋ} B)) \to A \lor_{ℋ} ((A \cap B) \lor_{ℋ} x) = A \lor_{ℋ} x$
26		ancom	$⊢ (x \subseteq B \land \neg x \subseteq A \cap B) \leftrightarrow (\neg x \subseteq A \cap B \land x \subseteq B)$
27		chnle	$⊢ (A \cap B \in C_{ℋ} \land x \in C_{ℋ}) \to (\neg x \subseteq A \cap B \leftrightarrow A \cap B \subset (A \cap B) \lor_{ℋ} x)$
28	3 27	mpan	$⊢ x \in C_{ℋ} \to (\neg x \subseteq A \cap B \leftrightarrow A \cap B \subset (A \cap B) \lor_{ℋ} x)$
29		inss2	$⊢ A \cap B \subseteq B$
30	29	biantrur	$⊢ x \subseteq B \leftrightarrow (A \cap B \subseteq B \land x \subseteq B)$
31		chlub	$⊢ (A \cap B \in C_{ℋ} \land x \in C_{ℋ} \land B \in C_{ℋ}) \to ((A \cap B \subseteq B \land x \subseteq B) \leftrightarrow (A \cap B) \lor_{ℋ} x \subseteq B)$
32	3 2 31	mp3an13	$⊢ x \in C_{ℋ} \to ((A \cap B \subseteq B \land x \subseteq B) \leftrightarrow (A \cap B) \lor_{ℋ} x \subseteq B)$
33	30 32	syl5bb	$⊢ x \in C_{ℋ} \to (x \subseteq B \leftrightarrow (A \cap B) \lor_{ℋ} x \subseteq B)$
34	28 33	anbi12d	$⊢ x \in C_{ℋ} \to ((\neg x \subseteq A \cap B \land x \subseteq B) \leftrightarrow (A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq B))$
35	26 34	syl5bb	$⊢ x \in C_{ℋ} \to ((x \subseteq B \land \neg x \subseteq A \cap B) \leftrightarrow (A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq B))$
36		chjcl	$⊢ (A \cap B \in C_{ℋ} \land x \in C_{ℋ}) \to (A \cap B) \lor_{ℋ} x \in C_{ℋ}$
37	3 36	mpan	$⊢ x \in C_{ℋ} \to (A \cap B) \lor_{ℋ} x \in C_{ℋ}$
38		cvnbtwn2	$⊢ (A \cap B \in C_{ℋ} \land B \in C_{ℋ} \land (A \cap B) \lor_{ℋ} x \in C_{ℋ}) \to ((A \cap B) ⋖_{ℋ} B \to ((A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq B) \to (A \cap B) \lor_{ℋ} x = B))$
39	3 2 38	mp3an12	$⊢ (A \cap B) \lor_{ℋ} x \in C_{ℋ} \to ((A \cap B) ⋖_{ℋ} B \to ((A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq B) \to (A \cap B) \lor_{ℋ} x = B))$
40	37 39	syl	$⊢ x \in C_{ℋ} \to ((A \cap B) ⋖_{ℋ} B \to ((A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq B) \to (A \cap B) \lor_{ℋ} x = B))$
41	40	com23	$⊢ x \in C_{ℋ} \to ((A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq B) \to ((A \cap B) ⋖_{ℋ} B \to (A \cap B) \lor_{ℋ} x = B))$
42	35 41	sylbid	$⊢ x \in C_{ℋ} \to ((x \subseteq B \land \neg x \subseteq A \cap B) \to ((A \cap B) ⋖_{ℋ} B \to (A \cap B) \lor_{ℋ} x = B))$
43	42	imp32	$⊢ (x \in C_{ℋ} \land ((x \subseteq B \land \neg x \subseteq A \cap B) \land (A \cap B) ⋖_{ℋ} B)) \to (A \cap B) \lor_{ℋ} x = B$
44	43	oveq2d	$⊢ (x \in C_{ℋ} \land ((x \subseteq B \land \neg x \subseteq A \cap B) \land (A \cap B) ⋖_{ℋ} B)) \to A \lor_{ℋ} ((A \cap B) \lor_{ℋ} x) = A \lor_{ℋ} B$
45	25 44	eqtr3d	$⊢ (x \in C_{ℋ} \land ((x \subseteq B \land \neg x \subseteq A \cap B) \land (A \cap B) ⋖_{ℋ} B)) \to A \lor_{ℋ} x = A \lor_{ℋ} B$
46	19 45	sylan	$⊢ (x \in HAtoms \land ((x \subseteq B \land \neg x \subseteq A \cap B) \land (A \cap B) ⋖_{ℋ} B)) \to A \lor_{ℋ} x = A \lor_{ℋ} B$
47	18 46	breqtrd	$⊢ (x \in HAtoms \land ((x \subseteq B \land \neg x \subseteq A \cap B) \land (A \cap B) ⋖_{ℋ} B)) \to A ⋖_{ℋ} (A \lor_{ℋ} B)$
48	47	exp32	$⊢ x \in HAtoms \to ((x \subseteq B \land \neg x \subseteq A \cap B) \to ((A \cap B) ⋖_{ℋ} B \to A ⋖_{ℋ} (A \lor_{ℋ} B)))$
49	48	rexlimiv	$⊢ \exists x \in HAtoms (x \subseteq B \land \neg x \subseteq A \cap B) \to ((A \cap B) ⋖_{ℋ} B \to A ⋖_{ℋ} (A \lor_{ℋ} B))$
50	7 49	mpcom	$⊢ (A \cap B) ⋖_{ℋ} B \to A ⋖_{ℋ} (A \lor_{ℋ} B)$

Metamath Proof Explorer

Theorem cvexchlem

Proof