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	bilani	$⊢ (r \subseteq B \land r \subseteq C) \to r \subseteq A \lor_{ℋ} p$
7	4 6	sylbir	$⊢ r \subseteq B \cap C \to r \subseteq A \lor_{ℋ} p$
8	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))$
9	8	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))))$
10	9	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))))$
11	10	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))))$
12	11	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))$
13	7 12	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))$
14	13	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))$
15	14	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))$
16	15	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))$
17	16	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))$
18	17	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)$
19		nssne2	$⊢ (q \subseteq A \land \neg r \subseteq A) \to q \neq r$
20	19	adantrl	$⊢ (q \subseteq A \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to q \neq r$
21		atnemeq0	$⊢ (q \in HAtoms \land r \in HAtoms) \to (q \neq r \leftrightarrow q \cap r = 0_{ℋ})$
22	21	ancoms	$⊢ (r \in HAtoms \land q \in HAtoms) \to (q \neq r \leftrightarrow q \cap r = 0_{ℋ})$
23	20 22	imbitrid	$⊢ (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_{ℋ})$
24	23	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_{ℋ})$
25	24	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_{ℋ})$
26		atelch	$⊢ p \in HAtoms \to p \in C_{ℋ}$
27		atelch	$⊢ q \in HAtoms \to q \in C_{ℋ}$
28		chjcom	$⊢ (p \in C_{ℋ} \land q \in C_{ℋ}) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
29	26 27 28	syl2an	$⊢ (p \in HAtoms \land q \in HAtoms) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
30	29	adantlr	$⊢ ((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \to p \lor_{ℋ} q = q \lor_{ℋ} p$
31	30	sseq2d	$⊢ ((p \in HAtoms \land r \in HAtoms) \land q \in HAtoms) \to (r \subseteq p \lor_{ℋ} q \leftrightarrow r \subseteq q \lor_{ℋ} p)$
32		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)$
33	27 32	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)$
34	33	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)$
35	34	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)$
36	35	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))$
37	31 36	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))$
38	37	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)$
39	25 38	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)$
40	39	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))$
41	40	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))))$
42	41	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))))$
43	42	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)))$
44	43	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)))$
45	44	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)$
46	45	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)$
47		simprl	$⊢ (q \in HAtoms \land (q \subseteq A \land r \subseteq p \lor_{ℋ} q)) \to q \subseteq A$
48	47	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)$
49		simpl	$⊢ (r \subseteq B \land r \subseteq C) \to r \subseteq B$
50	4 49	sylbir	$⊢ r \subseteq B \cap C \to r \subseteq B$
51	50	ad2antrl	$⊢ (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A)) \to r \subseteq B$
52	51	adantl	$⊢ (p \in HAtoms \land (r \in HAtoms \land (r \subseteq B \cap C \land \neg r \subseteq A))) \to r \subseteq B$
53	48 52	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))$
54	46 53	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)))$
55	54	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))))$
56	55	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))))$
57	56	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))))$
58	57	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))))$
59	58	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)))$
60	18 59	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))$
61		chjcl	$⊢ (A \in C_{ℋ} \land p \in C_{ℋ}) \to A \lor_{ℋ} p \in C_{ℋ}$
62	1 61	mpan	$⊢ p \in C_{ℋ} \to A \lor_{ℋ} p \in C_{ℋ}$
63	3 62	eqeltrid	$⊢ p \in C_{ℋ} \to C \in C_{ℋ}$
64		chincl	$⊢ (B \in C_{ℋ} \land C \in C_{ℋ}) \to B \cap C \in C_{ℋ}$
65	2 63 64	sylancr	$⊢ p \in C_{ℋ} \to B \cap C \in C_{ℋ}$
66	26 65	syl	$⊢ p \in HAtoms \to B \cap C \in C_{ℋ}$
67		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))$
68	66 1 67	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))$
69	68	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)$
70	69	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)$
71	60 70	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