mdsymlem3

Description: Lemma for mdsymi . (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdsymlem1.1	$⊢ A \in C_{ℋ}$
	mdsymlem1.2	$⊢ B \in C_{ℋ}$
	mdsymlem1.3	$⊢ C = A \lor_{ℋ} p$
Assertion	mdsymlem3	$⊢ (((p \in HAtoms \land \neg B \cap C \subseteq A) \land p \subseteq A \lor_{ℋ} B) \land A \neq 0_{ℋ}) \to \exists r \in HAtoms \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))$

Proof

Step	Hyp	Ref	Expression
1		mdsymlem1.1	$⊢ A \in C_{ℋ}$
2		mdsymlem1.2	$⊢ B \in C_{ℋ}$
3		mdsymlem1.3	$⊢ C = A \lor_{ℋ} p$
4		ssin	$⊢ (r \subseteq B \land r \subseteq C) \leftrightarrow r \subseteq B \cap C$
5	3	sseq2i	$⊢ r \subseteq C \leftrightarrow r \subseteq A \lor_{ℋ} p$
6	5	biimpi	$⊢ r \subseteq C \to r \subseteq A \lor_{ℋ} p$
7	6	adantl	$⊢ (r \subseteq B \land r \subseteq C) \to r \subseteq A \lor_{ℋ} p$
8	4 7	sylbir	$⊢ r \subseteq B \cap C \to r \subseteq A \lor_{ℋ} p$
9	1	atcvat4i	$⊢ (r \in HAtoms \land p \in HAtoms) \to ((A \neq 0_{ℋ} \land r \subseteq A \lor_{ℋ} p) \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))$
10	9	exp4b	$⊢ r \in HAtoms \to (p \in HAtoms \to (A \neq 0_{ℋ} \to (r \subseteq A \lor_{ℋ} p \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))))$
11	10	com34	$⊢ r \in HAtoms \to (p \in HAtoms \to (r \subseteq A \lor_{ℋ} p \to (A \neq 0_{ℋ} \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))))$
12	11	com23	$⊢ r \in HAtoms \to (r \subseteq A \lor_{ℋ} p \to (p \in HAtoms \to (A \neq 0_{ℋ} \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))))$
13	12	imp4b	$⊢ (r \in HAtoms \land r \subseteq A \lor_{ℋ} p) \to ((p \in HAtoms \land A \neq 0_{ℋ}) \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))$
14	8 13	sylan2	$⊢ (r \in HAtoms \land r \subseteq B \cap C) \to ((p \in HAtoms \land A \neq 0_{ℋ}) \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))$
15	14	adantrr	$⊢ (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to ((p \in HAtoms \land A \neq 0_{ℋ}) \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))$
16	15	com12	$⊢ (p \in HAtoms \land A \neq 0_{ℋ}) \to ((r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))$
17	16	adantlr	$⊢ ((p \in HAtoms \land \neg B \cap C \subseteq A) \land A \neq 0_{ℋ}) \to ((r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))$
18	17	adantlr	$⊢ (((p \in HAtoms \land \neg B \cap C \subseteq A) \land p \subseteq A \lor_{ℋ} B) \land A \neq 0_{ℋ}) \to ((r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q))$
19	18	imp	$⊢ ((((p \in HAtoms \land \neg B \cap C \subseteq A) \land p \subseteq A \lor_{ℋ} B) \land A \neq 0_{ℋ}) \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to \exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q)$
20		nssne2	$⊢ (q \subseteq A \land \neg r \subseteq A) \to q \neq r$
21	20	adantrl	$⊢ (q \subseteq A \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to q \neq r$
22		atnemeq0	$⊢ (q \in HAtoms \land r \in HAtoms) \to (q \neq r \leftrightarrow q \cap r = 0_{ℋ})$
23	22	ancoms	$⊢ (r \in HAtoms \land q \in HAtoms) \to (q \neq r \leftrightarrow q \cap r = 0_{ℋ})$
24	21 23	syl5ib	$⊢ (r \in HAtoms \land q \in HAtoms) \to ((q \subseteq A \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to q \cap r = 0_{ℋ})$
25	24	adantll	$⊢ ((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \to ((q \subseteq A \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to q \cap r = 0_{ℋ})$
26	25	adantr	$⊢ (((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \land r \subseteq p \lor_{ℋ} q) \to ((q \subseteq A \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to q \cap r = 0_{ℋ})$
27		atelch	$⊢ p \in HAtoms \to p \in C_{ℋ}$
28		atelch	$⊢ q \in HAtoms \to q \in C_{ℋ}$
29		chjcom	$⊢ (p \in C_{ℋ} \land q \in C_{ℋ}) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
30	27 28 29	syl2an	$⊢ (p \in HAtoms \land q \in HAtoms) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
31	30	adantlr	$⊢ ((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
32	31	sseq2d	$⊢ ((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \to (r \subseteq p \lor_{ℋ} q \leftrightarrow r \subseteq q \lor_{ℋ} p)$
33		atexch	$⊢ (q \in C_{ℋ} \land r \in HAtoms \land p \in HAtoms) \to ((r \subseteq q \lor_{ℋ} p \land q \cap r = 0_{ℋ}) \to p \subseteq q \lor_{ℋ} r)$
34	28 33	syl3an1	$⊢ (q \in HAtoms \land r \in HAtoms \land p \in HAtoms) \to ((r \subseteq q \lor_{ℋ} p \land q \cap r = 0_{ℋ}) \to p \subseteq q \lor_{ℋ} r)$
35	34	3com13	$⊢ (p \in HAtoms \land r \in HAtoms \land q \in HAtoms) \to ((r \subseteq q \lor_{ℋ} p \land q \cap r = 0_{ℋ}) \to p \subseteq q \lor_{ℋ} r)$
36	35	3expa	$⊢ ((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \to ((r \subseteq q \lor_{ℋ} p \land q \cap r = 0_{ℋ}) \to p \subseteq q \lor_{ℋ} r)$
37	36	expd	$⊢ ((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \to (r \subseteq q \lor_{ℋ} p \to (q \cap r = 0_{ℋ} \to p \subseteq q \lor_{ℋ} r))$
38	32 37	sylbid	$⊢ ((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \to (r \subseteq p \lor_{ℋ} q \to (q \cap r = 0_{ℋ} \to p \subseteq q \lor_{ℋ} r))$
39	38	imp	$⊢ (((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \land r \subseteq p \lor_{ℋ} q) \to (q \cap r = 0_{ℋ} \to p \subseteq q \lor_{ℋ} r)$
40	26 39	syld	$⊢ (((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \land r \subseteq p \lor_{ℋ} q) \to ((q \subseteq A \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to p \subseteq q \lor_{ℋ} r)$
41	40	expd	$⊢ (((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \land r \subseteq p \lor_{ℋ} q) \to (q \subseteq A \to ((r \subseteq B \cap C \land \neg r \subseteq A) \to p \subseteq q \lor_{ℋ} r))$
42	41	exp31	$⊢ (p \in HAtoms \land r \in HAtoms) \to (q \in HAtoms \to (r \subseteq p \lor_{ℋ} q \to (q \subseteq A \to ((r \subseteq B \cap C \land \neg r \subseteq A) \to p \subseteq q \lor_{ℋ} r))))$
43	42	com24	$⊢ (p \in HAtoms \land r \in HAtoms) \to (q \subseteq A \to (r \subseteq p \lor_{ℋ} q \to (q \in HAtoms \to ((r \subseteq B \cap C \land \neg r \subseteq A) \to p \subseteq q \lor_{ℋ} r))))$
44	43	impd	$⊢ (p \in HAtoms \land r \in HAtoms) \to ((q \subseteq A \land r \subseteq p \lor_{ℋ} q) \to (q \in HAtoms \to ((r \subseteq B \cap C \land \neg r \subseteq A) \to p \subseteq q \lor_{ℋ} r)))$
45	44	com24	$⊢ (p \in HAtoms \land r \in HAtoms) \to ((r \subseteq B \cap C \land \neg r \subseteq A) \to (q \in HAtoms \to ((q \subseteq A \land r \subseteq p \lor_{ℋ} q) \to p \subseteq q \lor_{ℋ} r)))$
46	45	imp4b	$⊢ ((p \in HAtoms \land r \in HAtoms) \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to ((q \in HAtoms \land (q \subseteq A \land r \subseteq p \lor_{ℋ} q)) \to p \subseteq q \lor_{ℋ} r)$
47	46	anasss	$⊢ (p \in HAtoms \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to ((q \in HAtoms \land (q \subseteq A \land r \subseteq p \lor_{ℋ} q)) \to p \subseteq q \lor_{ℋ} r)$
48		simprl	$⊢ (q \in HAtoms \land (q \subseteq A \land r \subseteq p \lor_{ℋ} q)) \to q \subseteq A$
49	48	a1i	$⊢ (p \in HAtoms \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to ((q \in HAtoms \land (q \subseteq A \land r \subseteq p \lor_{ℋ} q)) \to q \subseteq A)$
50		simpl	$⊢ (r \subseteq B \land r \subseteq C) \to r \subseteq B$
51	4 50	sylbir	$⊢ r \subseteq B \cap C \to r \subseteq B$
52	51	ad2antrl	$⊢ (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to r \subseteq B$
53	52	adantl	$⊢ (p \in HAtoms \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to r \subseteq B$
54	49 53	jctird	$⊢ (p \in HAtoms \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to ((q \in HAtoms \land (q \subseteq A \land r \subseteq p \lor_{ℋ} q)) \to (q \subseteq A \land r \subseteq B))$
55	47 54	jcad	$⊢ (p \in HAtoms \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to ((q \in HAtoms \land (q \subseteq A \land r \subseteq p \lor_{ℋ} q)) \to (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)))$
56	55	expd	$⊢ (p \in HAtoms \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to (q \in HAtoms \to ((q \subseteq A \land r \subseteq p \lor_{ℋ} q) \to (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))))$
57	56	adantlr	$⊢ ((p \in HAtoms \land \neg B \cap C \subseteq A) \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to (q \in HAtoms \to ((q \subseteq A \land r \subseteq p \lor_{ℋ} q) \to (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))))$
58	57	adantlr	$⊢ (((p \in HAtoms \land \neg B \cap C \subseteq A) \land p \subseteq A \lor_{ℋ} B) \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to (q \in HAtoms \to ((q \subseteq A \land r \subseteq p \lor_{ℋ} q) \to (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))))$
59	58	adantlr	$⊢ ((((p \in HAtoms \land \neg B \cap C \subseteq A) \land p \subseteq A \lor_{ℋ} B) \land A \neq 0_{ℋ}) \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to (q \in HAtoms \to ((q \subseteq A \land r \subseteq p \lor_{ℋ} q) \to (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))))$
60	59	reximdvai	$⊢ ((((p \in HAtoms \land \neg B \cap C \subseteq A) \land p \subseteq A \lor_{ℋ} B) \land A \neq 0_{ℋ}) \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to (\exists q \in HAtoms (q \subseteq A \land r \subseteq p \lor_{ℋ} q) \to \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)))$
61	19 60	mpd	$⊢ ((((p \in HAtoms \land \neg B \cap C \subseteq A) \land p \subseteq A \lor_{ℋ} B) \land A \neq 0_{ℋ}) \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))$
62		chjcl	$⊢ (A \in C_{ℋ} \land p \in C_{ℋ}) \to A \lor_{ℋ} p \in C_{ℋ}$
63	1 62	mpan	$⊢ p \in C_{ℋ} \to A \lor_{ℋ} p \in C_{ℋ}$
64	3 63	eqeltrid	$⊢ p \in C_{ℋ} \to C \in C_{ℋ}$
65		chincl	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to B \cap C \in C_{ℋ}$
66	2 64 65	sylancr	$⊢ p \in C_{ℋ} \to B \cap C \in C_{ℋ}$
67	27 66	syl	$⊢ p \in HAtoms \to B \cap C \in C_{ℋ}$
68		chrelat2	$⊢ (B \cap C \in C_{ℋ} \land A \in C_{ℋ}) \to (\neg B \cap C \subseteq A \leftrightarrow \exists r \in HAtoms (r \subseteq B \cap C \land \neg r \subseteq A))$
69	67 1 68	sylancl	$⊢ p \in HAtoms \to (\neg B \cap C \subseteq A \leftrightarrow \exists r \in HAtoms (r \subseteq B \cap C \land \neg r \subseteq A))$
70	69	biimpa	$⊢ (p \in HAtoms \land \neg B \cap C \subseteq A) \to \exists r \in HAtoms (r \subseteq B \cap C \land \neg r \subseteq A)$
71	70	ad2antrr	$⊢ (((p \in HAtoms \land \neg B \cap C \subseteq A) \land p \subseteq A \lor_{ℋ} B) \land A \neq 0_{ℋ}) \to \exists r \in HAtoms (r \subseteq B \cap C \land \neg r \subseteq A)$
72	61 71	reximddv	$⊢ (((p \in HAtoms \land \neg B \cap C \subseteq A) \land p \subseteq A \lor_{ℋ} B) \land A \neq 0_{ℋ}) \to \exists r \in HAtoms \exists q \in HAtoms (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))$

Metamath Proof Explorer

Theorem mdsymlem3

Proof