mdslmd1lem2

Description: Lemma for mdslmd1i . (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslmd.1	$⊢ A \in C_{ℋ}$
	mdslmd.2	$⊢ B \in C_{ℋ}$
	mdslmd.3	$⊢ C \in C_{ℋ}$
	mdslmd.4	$⊢ D \in C_{ℋ}$
	mdslmd1lem.5	$⊢ R \in C_{ℋ}$
Assertion	mdslmd1lem2	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \to ((R \cap B \subseteq D \cap B \to ((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B))) \to ((C \cap D \subseteq R \land R \subseteq D) \to (R \lor_{ℋ} C) \cap D \subseteq R \lor_{ℋ} (C \cap D)))$

Proof

Step	Hyp	Ref	Expression
1		mdslmd.1	$⊢ A \in C_{ℋ}$
2		mdslmd.2	$⊢ B \in C_{ℋ}$
3		mdslmd.3	$⊢ C \in C_{ℋ}$
4		mdslmd.4	$⊢ D \in C_{ℋ}$
5		mdslmd1lem.5	$⊢ R \in C_{ℋ}$
6		ssrin	$⊢ R \subseteq D \to R \cap B \subseteq D \cap B$
7	6	adantl	$⊢ (C \cap D \subseteq R \land R \subseteq D) \to R \cap B \subseteq D \cap B$
8	7	imim1i	$⊢ (R \cap B \subseteq D \cap B \to ((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B))) \to ((C \cap D \subseteq R \land R \subseteq D) \to ((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B)))$
9		simpllr	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to B 𝑀_{ℋ}^{} A$
10	3 5	chub2i	$⊢ C \subseteq R \lor_{ℋ} C$
11		sstr	$⊢ (A \subseteq C \land C \subseteq R \lor_{ℋ} C) \to A \subseteq R \lor_{ℋ} C$
12	10 11	mpan2	$⊢ A \subseteq C \to A \subseteq R \lor_{ℋ} C$
13	12	ad2antrr	$⊢ ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \to A \subseteq R \lor_{ℋ} C$
14	13	ad2antlr	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to A \subseteq R \lor_{ℋ} C$
15		simplr	$⊢ ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \to A \subseteq D$
16	15	ad2antlr	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to A \subseteq D$
17	14 16	ssind	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to A \subseteq (R \lor_{ℋ} C) \cap D$
18		ssin	$⊢ (A \subseteq C \land A \subseteq D) \leftrightarrow A \subseteq C \cap D$
19	3 4	chincli	$⊢ C \cap D \in C_{ℋ}$
20	19 5	chub2i	$⊢ C \cap D \subseteq R \lor_{ℋ} (C \cap D)$
21		sstr	$⊢ (A \subseteq C \cap D \land C \cap D \subseteq R \lor_{ℋ} (C \cap D)) \to A \subseteq R \lor_{ℋ} (C \cap D)$
22	20 21	mpan2	$⊢ A \subseteq C \cap D \to A \subseteq R \lor_{ℋ} (C \cap D)$
23	18 22	sylbi	$⊢ (A \subseteq C \land A \subseteq D) \to A \subseteq R \lor_{ℋ} (C \cap D)$
24	23	adantr	$⊢ ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \to A \subseteq R \lor_{ℋ} (C \cap D)$
25	24	ad2antlr	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to A \subseteq R \lor_{ℋ} (C \cap D)$
26	17 25	ssind	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to A \subseteq ((R \lor_{ℋ} C) \cap D) \cap (R \lor_{ℋ} (C \cap D))$
27		inss2	$⊢ (R \lor_{ℋ} C) \cap D \subseteq D$
28		sstr	$⊢ ((R \lor_{ℋ} C) \cap D \subseteq D \land D \subseteq A \lor_{ℋ} B) \to (R \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B$
29	27 28	mpan	$⊢ D \subseteq A \lor_{ℋ} B \to (R \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B$
30	29	ad2antll	$⊢ ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \to (R \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B$
31	30	ad2antlr	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to (R \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B$
32		sstr	$⊢ (R \subseteq D \land D \subseteq A \lor_{ℋ} B) \to R \subseteq A \lor_{ℋ} B$
33	32	ancoms	$⊢ (D \subseteq A \lor_{ℋ} B \land R \subseteq D) \to R \subseteq A \lor_{ℋ} B$
34	33	ad2ant2l	$⊢ ((C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B) \land (C \cap D \subseteq R \land R \subseteq D)) \to R \subseteq A \lor_{ℋ} B$
35	34	adantll	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D)) \to R \subseteq A \lor_{ℋ} B$
36	35	adantll	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to R \subseteq A \lor_{ℋ} B$
37		ssinss1	$⊢ C \subseteq A \lor_{ℋ} B \to C \cap D \subseteq A \lor_{ℋ} B$
38	37	ad2antrl	$⊢ ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \to C \cap D \subseteq A \lor_{ℋ} B$
39	38	ad2antlr	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to C \cap D \subseteq A \lor_{ℋ} B$
40	36 39	jca	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to (R \subseteq A \lor_{ℋ} B \land C \cap D \subseteq A \lor_{ℋ} B)$
41	1 2	chjcli	$⊢ A \lor_{ℋ} B \in C_{ℋ}$
42	5 19 41	chlubi	$⊢ (R \subseteq A \lor_{ℋ} B \land C \cap D \subseteq A \lor_{ℋ} B) \leftrightarrow R \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B$
43	40 42	sylib	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to R \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B$
44	31 43	jca	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to ((R \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B \land R \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B)$
45	5 3	chjcli	$⊢ R \lor_{ℋ} C \in C_{ℋ}$
46	45 4	chincli	$⊢ (R \lor_{ℋ} C) \cap D \in C_{ℋ}$
47	5 19	chjcli	$⊢ R \lor_{ℋ} (C \cap D) \in C_{ℋ}$
48	46 47 41	chlubi	$⊢ ((R \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B \land R \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B) \leftrightarrow ((R \lor_{ℋ} C) \cap D) \lor_{ℋ} (R \lor_{ℋ} (C \cap D)) \subseteq A \lor_{ℋ} B$
49	44 48	sylib	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to ((R \lor_{ℋ} C) \cap D) \lor_{ℋ} (R \lor_{ℋ} (C \cap D)) \subseteq A \lor_{ℋ} B$
50	1 2 46 47	mdslle1i	$⊢ (B 𝑀_{ℋ}^{*} A \land A \subseteq ((R \lor_{ℋ} C) \cap D) \cap (R \lor_{ℋ} (C \cap D)) \land ((R \lor_{ℋ} C) \cap D) \lor_{ℋ} (R \lor_{ℋ} (C \cap D)) \subseteq A \lor_{ℋ} B) \to ((R \lor_{ℋ} C) \cap D \subseteq R \lor_{ℋ} (C \cap D) \leftrightarrow ((R \lor_{ℋ} C) \cap D) \cap B \subseteq (R \lor_{ℋ} (C \cap D)) \cap B)$
51	9 26 49 50	syl3anc	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to ((R \lor_{ℋ} C) \cap D \subseteq R \lor_{ℋ} (C \cap D) \leftrightarrow ((R \lor_{ℋ} C) \cap D) \cap B \subseteq (R \lor_{ℋ} (C \cap D)) \cap B)$
52		inindir	$⊢ ((R \lor_{ℋ} C) \cap D) \cap B = ((R \lor_{ℋ} C) \cap B) \cap (D \cap B)$
53		sstr	$⊢ (A \subseteq C \cap D \land C \cap D \subseteq R) \to A \subseteq R$
54	18 53	sylanb	$⊢ ((A \subseteq C \land A \subseteq D) \land C \cap D \subseteq R) \to A \subseteq R$
55	54	ad2ant2r	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D)) \to A \subseteq R$
56		simplll	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D)) \to A \subseteq C$
57	55 56	ssind	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D)) \to A \subseteq R \cap C$
58		simplrl	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D)) \to C \subseteq A \lor_{ℋ} B$
59	35 58	jca	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D)) \to (R \subseteq A \lor_{ℋ} B \land C \subseteq A \lor_{ℋ} B)$
60	5 3 41	chlubi	$⊢ (R \subseteq A \lor_{ℋ} B \land C \subseteq A \lor_{ℋ} B) \leftrightarrow R \lor_{ℋ} C \subseteq A \lor_{ℋ} B$
61	59 60	sylib	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D)) \to R \lor_{ℋ} C \subseteq A \lor_{ℋ} B$
62	57 61	jca	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D)) \to (A \subseteq R \cap C \land R \lor_{ℋ} C \subseteq A \lor_{ℋ} B)$
63	1 2 5 3	mdslj1i	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land (A \subseteq R \cap C \land R \lor_{ℋ} C \subseteq A \lor_{ℋ} B)) \to (R \lor_{ℋ} C) \cap B = (R \cap B) \lor_{ℋ} (C \cap B)$
64	62 63	sylan2	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D))) \to (R \lor_{ℋ} C) \cap B = (R \cap B) \lor_{ℋ} (C \cap B)$
65	64	anassrs	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to (R \lor_{ℋ} C) \cap B = (R \cap B) \lor_{ℋ} (C \cap B)$
66	65	ineq1d	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to ((R \lor_{ℋ} C) \cap B) \cap (D \cap B) = ((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B)$
67	52 66	eqtr2id	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to ((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B) = ((R \lor_{ℋ} C) \cap D) \cap B$
68	18	birani	$⊢ ((A \subseteq C \land A \subseteq D) \land C \cap D \subseteq R) \to A \subseteq C \cap D$
69	54 68	ssind	$⊢ ((A \subseteq C \land A \subseteq D) \land C \cap D \subseteq R) \to A \subseteq R \cap (C \cap D)$
70	33	adantll	$⊢ ((C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B) \land R \subseteq D) \to R \subseteq A \lor_{ℋ} B$
71	37	ad2antrr	$⊢ ((C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B) \land R \subseteq D) \to C \cap D \subseteq A \lor_{ℋ} B$
72	70 71	jca	$⊢ ((C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B) \land R \subseteq D) \to (R \subseteq A \lor_{ℋ} B \land C \cap D \subseteq A \lor_{ℋ} B)$
73	72 42	sylib	$⊢ ((C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B) \land R \subseteq D) \to R \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B$
74	69 73	anim12i	$⊢ (((A \subseteq C \land A \subseteq D) \land C \cap D \subseteq R) \land ((C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B) \land R \subseteq D)) \to (A \subseteq R \cap (C \cap D) \land R \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B)$
75	74	an4s	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D)) \to (A \subseteq R \cap (C \cap D) \land R \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B)$
76	1 2 5 19	mdslj1i	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land (A \subseteq R \cap (C \cap D) \land R \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B)) \to (R \lor_{ℋ} (C \cap D)) \cap B = (R \cap B) \lor_{ℋ} ((C \cap D) \cap B)$
77	75 76	sylan2	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land (C \cap D \subseteq R \land R \subseteq D))) \to (R \lor_{ℋ} (C \cap D)) \cap B = (R \cap B) \lor_{ℋ} ((C \cap D) \cap B)$
78	77	anassrs	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to (R \lor_{ℋ} (C \cap D)) \cap B = (R \cap B) \lor_{ℋ} ((C \cap D) \cap B)$
79		inindir	$⊢ (C \cap D) \cap B = (C \cap B) \cap (D \cap B)$
80	79	a1i	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to (C \cap D) \cap B = (C \cap B) \cap (D \cap B)$
81	80	oveq2d	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to (R \cap B) \lor_{ℋ} ((C \cap D) \cap B) = (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B))$
82	78 81	eqtr2d	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B)) = (R \lor_{ℋ} (C \cap D)) \cap B$
83	67 82	sseq12d	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to (((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B)) \leftrightarrow ((R \lor_{ℋ} C) \cap D) \cap B \subseteq (R \lor_{ℋ} (C \cap D)) \cap B)$
84	51 83	bitr4d	$⊢ (((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \land (C \cap D \subseteq R \land R \subseteq D)) \to ((R \lor_{ℋ} C) \cap D \subseteq R \lor_{ℋ} (C \cap D) \leftrightarrow ((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B)))$
85	84	exbiri	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \to ((C \cap D \subseteq R \land R \subseteq D) \to (((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B)) \to (R \lor_{ℋ} C) \cap D \subseteq R \lor_{ℋ} (C \cap D)))$
86	85	a2d	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \to (((C \cap D \subseteq R \land R \subseteq D) \to ((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B))) \to ((C \cap D \subseteq R \land R \subseteq D) \to (R \lor_{ℋ} C) \cap D \subseteq R \lor_{ℋ} (C \cap D)))$
87	8 86	syl5	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B))) \to ((R \cap B \subseteq D \cap B \to ((R \cap B) \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq (R \cap B) \lor_{ℋ} ((C \cap B) \cap (D \cap B))) \to ((C \cap D \subseteq R \land R \subseteq D) \to (R \lor_{ℋ} C) \cap D \subseteq R \lor_{ℋ} (C \cap D)))$

Metamath Proof Explorer

Theorem mdslmd1lem2

Proof