mdsymlem5

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	mdsymlem5	$⊢ (q \in HAtoms \land r \in HAtoms) \to (\neg q = p \to ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \to (((c \in C_{ℋ} \land A \subseteq c) \land p \in HAtoms) \to (p \subseteq c \to p \subseteq (c \cap B) \lor_{ℋ} A))))$

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		df-ne	$⊢ q \neq p \leftrightarrow \neg q = p$
5		atnemeq0	$⊢ (q \in HAtoms \land p \in HAtoms) \to (q \neq p \leftrightarrow q \cap p = 0_{ℋ})$
6	4 5	bitr3id	$⊢ (q \in HAtoms \land p \in HAtoms) \to (\neg q = p \leftrightarrow q \cap p = 0_{ℋ})$
7	6	anbi2d	$⊢ (q \in HAtoms \land p \in HAtoms) \to ((p \subseteq q \lor_{ℋ} r \land \neg q = p) \leftrightarrow (p \subseteq q \lor_{ℋ} r \land q \cap p = 0_{ℋ}))$
8	7	3adant3	$⊢ (q \in HAtoms \land p \in HAtoms \land r \in HAtoms) \to ((p \subseteq q \lor_{ℋ} r \land \neg q = p) \leftrightarrow (p \subseteq q \lor_{ℋ} r \land q \cap p = 0_{ℋ}))$
9		atelch	$⊢ q \in HAtoms \to q \in C_{ℋ}$
10		atexch	$⊢ (q \in C_{ℋ} \land p \in HAtoms \land r \in HAtoms) \to ((p \subseteq q \lor_{ℋ} r \land q \cap p = 0_{ℋ}) \to r \subseteq q \lor_{ℋ} p)$
11	9 10	syl3an1	$⊢ (q \in HAtoms \land p \in HAtoms \land r \in HAtoms) \to ((p \subseteq q \lor_{ℋ} r \land q \cap p = 0_{ℋ}) \to r \subseteq q \lor_{ℋ} p)$
12	8 11	sylbid	$⊢ (q \in HAtoms \land p \in HAtoms \land r \in HAtoms) \to ((p \subseteq q \lor_{ℋ} r \land \neg q = p) \to r \subseteq q \lor_{ℋ} p)$
13	12	expd	$⊢ (q \in HAtoms \land p \in HAtoms \land r \in HAtoms) \to (p \subseteq q \lor_{ℋ} r \to (\neg q = p \to r \subseteq q \lor_{ℋ} p))$
14	13	3com23	$⊢ (q \in HAtoms \land r \in HAtoms \land p \in HAtoms) \to (p \subseteq q \lor_{ℋ} r \to (\neg q = p \to r \subseteq q \lor_{ℋ} p))$
15	14	3expa	$⊢ ((q \in HAtoms \land r \in HAtoms) \land p \in HAtoms) \to (p \subseteq q \lor_{ℋ} r \to (\neg q = p \to r \subseteq q \lor_{ℋ} p))$
16	15	adantrl	$⊢ ((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \to (p \subseteq q \lor_{ℋ} r \to (\neg q = p \to r \subseteq q \lor_{ℋ} p))$
17	16	adantrd	$⊢ ((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \to ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \to (\neg q = p \to r \subseteq q \lor_{ℋ} p))$
18	17	imp32	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \to r \subseteq q \lor_{ℋ} p$
19	18	adantrl	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land (A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p))) \to r \subseteq q \lor_{ℋ} p$
20	19	adantrr	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land ((A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \land p \subseteq c)) \to r \subseteq q \lor_{ℋ} p$
21		simplrl	$⊢ ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p) \to q \subseteq A$
22		atelch	$⊢ p \in HAtoms \to p \in C_{ℋ}$
23	22	anim1i	$⊢ (p \in HAtoms \land c \in C_{ℋ}) \to (p \in C_{ℋ} \land c \in C_{ℋ})$
24	23	ancoms	$⊢ (c \in C_{ℋ} \land p \in HAtoms) \to (p \in C_{ℋ} \land c \in C_{ℋ})$
25		chub2	$⊢ (A \in C_{ℋ} \land c \in C_{ℋ}) \to A \subseteq c \lor_{ℋ} A$
26	1 25	mpan	$⊢ c \in C_{ℋ} \to A \subseteq c \lor_{ℋ} A$
27		sstr	$⊢ (q \subseteq A \land A \subseteq c \lor_{ℋ} A) \to q \subseteq c \lor_{ℋ} A$
28	26 27	sylan2	$⊢ (q \subseteq A \land c \in C_{ℋ}) \to q \subseteq c \lor_{ℋ} A$
29		chub1	$⊢ (c \in C_{ℋ} \land A \in C_{ℋ}) \to c \subseteq c \lor_{ℋ} A$
30	1 29	mpan2	$⊢ c \in C_{ℋ} \to c \subseteq c \lor_{ℋ} A$
31		sstr	$⊢ (p \subseteq c \land c \subseteq c \lor_{ℋ} A) \to p \subseteq c \lor_{ℋ} A$
32	30 31	sylan2	$⊢ (p \subseteq c \land c \in C_{ℋ}) \to p \subseteq c \lor_{ℋ} A$
33	28 32	anim12i	$⊢ ((q \subseteq A \land c \in C_{ℋ}) \land (p \subseteq c \land c \in C_{ℋ})) \to (q \subseteq c \lor_{ℋ} A \land p \subseteq c \lor_{ℋ} A)$
34	33	anandirs	$⊢ ((q \subseteq A \land p \subseteq c) \land c \in C_{ℋ}) \to (q \subseteq c \lor_{ℋ} A \land p \subseteq c \lor_{ℋ} A)$
35	34	ancoms	$⊢ (c \in C_{ℋ} \land (q \subseteq A \land p \subseteq c)) \to (q \subseteq c \lor_{ℋ} A \land p \subseteq c \lor_{ℋ} A)$
36	35	adantll	$⊢ (((q \in C_{ℋ} \land p \in C_{ℋ}) \land c \in C_{ℋ}) \land (q \subseteq A \land p \subseteq c)) \to (q \subseteq c \lor_{ℋ} A \land p \subseteq c \lor_{ℋ} A)$
37		chjcl	$⊢ (c \in C_{ℋ} \land A \in C_{ℋ}) \to c \lor_{ℋ} A \in C_{ℋ}$
38	1 37	mpan2	$⊢ c \in C_{ℋ} \to c \lor_{ℋ} A \in C_{ℋ}$
39		chlub	$⊢ (q \in C_{ℋ} \land p \in C_{ℋ} \land c \lor_{ℋ} A \in C_{ℋ}) \to ((q \subseteq c \lor_{ℋ} A \land p \subseteq c \lor_{ℋ} A) \leftrightarrow q \lor_{ℋ} p \subseteq c \lor_{ℋ} A)$
40	38 39	syl3an3	$⊢ (q \in C_{ℋ} \land p \in C_{ℋ} \land c \in C_{ℋ}) \to ((q \subseteq c \lor_{ℋ} A \land p \subseteq c \lor_{ℋ} A) \leftrightarrow q \lor_{ℋ} p \subseteq c \lor_{ℋ} A)$
41	40	3expa	$⊢ ((q \in C_{ℋ} \land p \in C_{ℋ}) \land c \in C_{ℋ}) \to ((q \subseteq c \lor_{ℋ} A \land p \subseteq c \lor_{ℋ} A) \leftrightarrow q \lor_{ℋ} p \subseteq c \lor_{ℋ} A)$
42	41	adantr	$⊢ (((q \in C_{ℋ} \land p \in C_{ℋ}) \land c \in C_{ℋ}) \land (q \subseteq A \land p \subseteq c)) \to ((q \subseteq c \lor_{ℋ} A \land p \subseteq c \lor_{ℋ} A) \leftrightarrow q \lor_{ℋ} p \subseteq c \lor_{ℋ} A)$
43	36 42	mpbid	$⊢ (((q \in C_{ℋ} \land p \in C_{ℋ}) \land c \in C_{ℋ}) \land (q \subseteq A \land p \subseteq c)) \to q \lor_{ℋ} p \subseteq c \lor_{ℋ} A$
44	43	adantrl	$⊢ (((q \in C_{ℋ} \land p \in C_{ℋ}) \land c \in C_{ℋ}) \land (A \subseteq c \land (q \subseteq A \land p \subseteq c))) \to q \lor_{ℋ} p \subseteq c \lor_{ℋ} A$
45		chlejb2	$⊢ (A \in C_{ℋ} \land c \in C_{ℋ}) \to (A \subseteq c \leftrightarrow c \lor_{ℋ} A = c)$
46	1 45	mpan	$⊢ c \in C_{ℋ} \to (A \subseteq c \leftrightarrow c \lor_{ℋ} A = c)$
47	46	biimpa	$⊢ (c \in C_{ℋ} \land A \subseteq c) \to c \lor_{ℋ} A = c$
48	47	ad2ant2lr	$⊢ (((q \in C_{ℋ} \land p \in C_{ℋ}) \land c \in C_{ℋ}) \land (A \subseteq c \land (q \subseteq A \land p \subseteq c))) \to c \lor_{ℋ} A = c$
49	44 48	sseqtrd	$⊢ (((q \in C_{ℋ} \land p \in C_{ℋ}) \land c \in C_{ℋ}) \land (A \subseteq c \land (q \subseteq A \land p \subseteq c))) \to q \lor_{ℋ} p \subseteq c$
50	49	exp45	$⊢ ((q \in C_{ℋ} \land p \in C_{ℋ}) \land c \in C_{ℋ}) \to (A \subseteq c \to (q \subseteq A \to (p \subseteq c \to q \lor_{ℋ} p \subseteq c)))$
51	50	anasss	$⊢ (q \in C_{ℋ} \land (p \in C_{ℋ} \land c \in C_{ℋ})) \to (A \subseteq c \to (q \subseteq A \to (p \subseteq c \to q \lor_{ℋ} p \subseteq c)))$
52	9 24 51	syl2an	$⊢ (q \in HAtoms \land (c \in C_{ℋ} \land p \in HAtoms)) \to (A \subseteq c \to (q \subseteq A \to (p \subseteq c \to q \lor_{ℋ} p \subseteq c)))$
53	52	adantlr	$⊢ ((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \to (A \subseteq c \to (q \subseteq A \to (p \subseteq c \to q \lor_{ℋ} p \subseteq c)))$
54	21 53	syl7	$⊢ ((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \to (A \subseteq c \to (((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p) \to (p \subseteq c \to q \lor_{ℋ} p \subseteq c)))$
55	54	imp44	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land ((A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \land p \subseteq c)) \to q \lor_{ℋ} p \subseteq c$
56	20 55	sstrd	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land ((A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \land p \subseteq c)) \to r \subseteq c$
57		simplrr	$⊢ ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p) \to r \subseteq B$
58	57	ad2antlr	$⊢ ((A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \land p \subseteq c) \to r \subseteq B$
59	58	adantl	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land ((A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \land p \subseteq c)) \to r \subseteq B$
60	56 59	ssind	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land ((A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \land p \subseteq c)) \to r \subseteq c \cap B$
61		atelch	$⊢ r \in HAtoms \to r \in C_{ℋ}$
62	9 61	anim12i	$⊢ (q \in HAtoms \land r \in HAtoms) \to (q \in C_{ℋ} \land r \in C_{ℋ})$
63		chincl	$⊢ (c \in C_{ℋ} \land B \in C_{ℋ}) \to c \cap B \in C_{ℋ}$
64	2 63	mpan2	$⊢ c \in C_{ℋ} \to c \cap B \in C_{ℋ}$
65		chlej1	$⊢ ((r \in C_{ℋ} \land c \cap B \in C_{ℋ} \land q \in C_{ℋ}) \land r \subseteq c \cap B) \to r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} q$
66	65	ex	$⊢ (r \in C_{ℋ} \land c \cap B \in C_{ℋ} \land q \in C_{ℋ}) \to (r \subseteq c \cap B \to r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} q)$
67	64 66	syl3an2	$⊢ (r \in C_{ℋ} \land c \in C_{ℋ} \land q \in C_{ℋ}) \to (r \subseteq c \cap B \to r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} q)$
68	67	3comr	$⊢ (q \in C_{ℋ} \land r \in C_{ℋ} \land c \in C_{ℋ}) \to (r \subseteq c \cap B \to r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} q)$
69	68	3expa	$⊢ ((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \to (r \subseteq c \cap B \to r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} q)$
70	69	adantr	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land q \subseteq A) \to (r \subseteq c \cap B \to r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} q)$
71		chlej2	$⊢ ((q \in C_{ℋ} \land A \in C_{ℋ} \land c \cap B \in C_{ℋ}) \land q \subseteq A) \to (c \cap B) \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} A$
72	1 71	mp3anl2	$⊢ ((q \in C_{ℋ} \land c \cap B \in C_{ℋ}) \land q \subseteq A) \to (c \cap B) \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} A$
73	64 72	sylanl2	$⊢ ((q \in C_{ℋ} \land c \in C_{ℋ}) \land q \subseteq A) \to (c \cap B) \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} A$
74	73	adantllr	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land q \subseteq A) \to (c \cap B) \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} A$
75		sstr2	$⊢ r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} q \to ((c \cap B) \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} A \to r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} A)$
76	74 75	syl5com	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land q \subseteq A) \to (r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} q \to r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} A)$
77		chjcom	$⊢ (q \in C_{ℋ} \land r \in C_{ℋ}) \to q \lor_{ℋ} r = r \lor_{ℋ} q$
78	77	ad2antrr	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land q \subseteq A) \to q \lor_{ℋ} r = r \lor_{ℋ} q$
79	78	sseq1d	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land q \subseteq A) \to (q \lor_{ℋ} r \subseteq (c \cap B) \lor_{ℋ} A \leftrightarrow r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} A)$
80	76 79	sylibrd	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land q \subseteq A) \to (r \lor_{ℋ} q \subseteq (c \cap B) \lor_{ℋ} q \to q \lor_{ℋ} r \subseteq (c \cap B) \lor_{ℋ} A)$
81	70 80	syld	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land q \subseteq A) \to (r \subseteq c \cap B \to q \lor_{ℋ} r \subseteq (c \cap B) \lor_{ℋ} A)$
82	81	adantrl	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land (p \subseteq q \lor_{ℋ} r \land q \subseteq A)) \to (r \subseteq c \cap B \to q \lor_{ℋ} r \subseteq (c \cap B) \lor_{ℋ} A)$
83		sstr2	$⊢ p \subseteq q \lor_{ℋ} r \to (q \lor_{ℋ} r \subseteq (c \cap B) \lor_{ℋ} A \to p \subseteq (c \cap B) \lor_{ℋ} A)$
84	83	ad2antrl	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land (p \subseteq q \lor_{ℋ} r \land q \subseteq A)) \to (q \lor_{ℋ} r \subseteq (c \cap B) \lor_{ℋ} A \to p \subseteq (c \cap B) \lor_{ℋ} A)$
85	82 84	syld	$⊢ (((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \land (p \subseteq q \lor_{ℋ} r \land q \subseteq A)) \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)$
86	85	exp32	$⊢ ((q \in C_{ℋ} \land r \in C_{ℋ}) \land c \in C_{ℋ}) \to (p \subseteq q \lor_{ℋ} r \to (q \subseteq A \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)))$
87	62 86	sylan	$⊢ ((q \in HAtoms \land r \in HAtoms) \land c \in C_{ℋ}) \to (p \subseteq q \lor_{ℋ} r \to (q \subseteq A \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)))$
88	87	adantrr	$⊢ ((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \to (p \subseteq q \lor_{ℋ} r \to (q \subseteq A \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)))$
89	88	imp31	$⊢ ((((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land p \subseteq q \lor_{ℋ} r) \land q \subseteq A) \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)$
90	89	adantrr	$⊢ ((((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land p \subseteq q \lor_{ℋ} r) \land (q \subseteq A \land r \subseteq B)) \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)$
91	90	anasss	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land (p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B))) \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)$
92	91	adantrr	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)$
93	92	adantrl	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land (A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p))) \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)$
94	93	adantrr	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land ((A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \land p \subseteq c)) \to (r \subseteq c \cap B \to p \subseteq (c \cap B) \lor_{ℋ} A)$
95	60 94	mpd	$⊢ (((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \land ((A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \land p \subseteq c)) \to p \subseteq (c \cap B) \lor_{ℋ} A$
96	95	exp32	$⊢ ((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \to ((A \subseteq c \land ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \land \neg q = p)) \to (p \subseteq c \to p \subseteq (c \cap B) \lor_{ℋ} A))$
97	96	exp4d	$⊢ ((q \in HAtoms \land r \in HAtoms) \land (c \in C_{ℋ} \land p \in HAtoms)) \to (A \subseteq c \to ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \to (\neg q = p \to (p \subseteq c \to p \subseteq (c \cap B) \lor_{ℋ} A))))$
98	97	exp32	$⊢ (q \in HAtoms \land r \in HAtoms) \to (c \in C_{ℋ} \to (p \in HAtoms \to (A \subseteq c \to ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \to (\neg q = p \to (p \subseteq c \to p \subseteq (c \cap B) \lor_{ℋ} A))))))$
99	98	com34	$⊢ (q \in HAtoms \land r \in HAtoms) \to (c \in C_{ℋ} \to (A \subseteq c \to (p \in HAtoms \to ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \to (\neg q = p \to (p \subseteq c \to p \subseteq (c \cap B) \lor_{ℋ} A))))))$
100	99	imp4c	$⊢ (q \in HAtoms \land r \in HAtoms) \to (((c \in C_{ℋ} \land A \subseteq c) \land p \in HAtoms) \to ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \to (\neg q = p \to (p \subseteq c \to p \subseteq (c \cap B) \lor_{ℋ} A))))$
101	100	com24	$⊢ (q \in HAtoms \land r \in HAtoms) \to (\neg q = p \to ((p \subseteq q \lor_{ℋ} r \land (q \subseteq A \land r \subseteq B)) \to (((c \in C_{ℋ} \land A \subseteq c) \land p \in HAtoms) \to (p \subseteq c \to p \subseteq (c \cap B) \lor_{ℋ} A))))$

Metamath Proof Explorer

Theorem mdsymlem5

Proof