mdslmd1lem1

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	mdslmd1lem1	$⊢ ((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 \lor_{ℋ} A \subseteq D \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \to (((C \cap B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B) \to (R \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq R \lor_{ℋ} ((C \cap B) \cap (D \cap B))))$

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	4 2	chincli	$⊢ D \cap B \in C_{ℋ}$
7	5 6 1	chlej1i	$⊢ R \subseteq D \cap B \to R \lor_{ℋ} A \subseteq (D \cap B) \lor_{ℋ} A$
8		simpr	$⊢ (A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{} A) \to B 𝑀_{ℋ}^{} A$
9		simpr	$⊢ (A \subseteq C \land A \subseteq D) \to A \subseteq D$
10		simpr	$⊢ (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B) \to D \subseteq A \lor_{ℋ} B$
11	1 2 4	3pm3.2i	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land D \in C_{ℋ})$
12		dmdsl3	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land D \in C_{ℋ}) \land (B 𝑀_{ℋ}^{*} A \land A \subseteq D \land D \subseteq A \lor_{ℋ} B)) \to (D \cap B) \lor_{ℋ} A = D$
13	11 12	mpan	$⊢ (B 𝑀_{ℋ}^{*} A \land A \subseteq D \land D \subseteq A \lor_{ℋ} B) \to (D \cap B) \lor_{ℋ} A = D$
14	8 9 10 13	syl3an	$⊢ ((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 (D \cap B) \lor_{ℋ} A = D$
15	14	3expb	$⊢ ((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 (D \cap B) \lor_{ℋ} A = D$
16	15	sseq2d	$⊢ ((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 \lor_{ℋ} A \subseteq (D \cap B) \lor_{ℋ} A \leftrightarrow R \lor_{ℋ} A \subseteq D)$
17	7 16	syl5ib	$⊢ ((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 \subseteq D \cap B \to R \lor_{ℋ} A \subseteq D)$
18	17	adantld	$⊢ ((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B) \to R \lor_{ℋ} A \subseteq D)$
19	18	imim1d	$⊢ ((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 \lor_{ℋ} A \subseteq D \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \to (((C \cap B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B) \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)))$
20		simpll	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{} A)$
21		simpll	$⊢ ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \to A \subseteq C$
22	21	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \subseteq C$
23	1 5	chub2i	$⊢ A \subseteq R \lor_{ℋ} A$
24	22 23	jctil	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (A \subseteq R \lor_{ℋ} A \land A \subseteq C)$
25		ssin	$⊢ (A \subseteq R \lor_{ℋ} A \land A \subseteq C) \leftrightarrow A \subseteq (R \lor_{ℋ} A) \cap C$
26	24 25	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \subseteq (R \lor_{ℋ} A) \cap C$
27		inss1	$⊢ D \cap B \subseteq D$
28		sstr	$⊢ (R \subseteq D \cap B \land D \cap B \subseteq D) \to R \subseteq D$
29	27 28	mpan2	$⊢ R \subseteq D \cap B \to R \subseteq D$
30		sstr	$⊢ (R \subseteq D \land D \subseteq A \lor_{ℋ} B) \to R \subseteq A \lor_{ℋ} B$
31	29 30	sylan	$⊢ (R \subseteq D \cap B \land D \subseteq A \lor_{ℋ} B) \to R \subseteq A \lor_{ℋ} B$
32	31	ancoms	$⊢ (D \subseteq A \lor_{ℋ} B \land R \subseteq D \cap B) \to R \subseteq A \lor_{ℋ} B$
33	32	adantll	$⊢ ((C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B) \land R \subseteq D \cap B) \to R \subseteq A \lor_{ℋ} B$
34	33	adantll	$⊢ (((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \land R \subseteq D \cap B) \to R \subseteq A \lor_{ℋ} B$
35	34	ad2ant2l	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to R \subseteq A \lor_{ℋ} B$
36	1 2	chub1i	$⊢ A \subseteq A \lor_{ℋ} B$
37	35 36	jctir	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (R \subseteq A \lor_{ℋ} B \land A \subseteq A \lor_{ℋ} B)$
38	1 2	chjcli	$⊢ A \lor_{ℋ} B \in C_{ℋ}$
39	5 1 38	chlubi	$⊢ (R \subseteq A \lor_{ℋ} B \land A \subseteq A \lor_{ℋ} B) \leftrightarrow R \lor_{ℋ} A \subseteq A \lor_{ℋ} B$
40	37 39	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to R \lor_{ℋ} A \subseteq A \lor_{ℋ} B$
41		simprrl	$⊢ ((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 \subseteq A \lor_{ℋ} B$
42	41	adantr	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to C \subseteq A \lor_{ℋ} B$
43	40 42	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (R \lor_{ℋ} A \subseteq A \lor_{ℋ} B \land C \subseteq A \lor_{ℋ} B)$
44	5 1	chjcli	$⊢ R \lor_{ℋ} A \in C_{ℋ}$
45	44 3 38	chlubi	$⊢ (R \lor_{ℋ} A \subseteq A \lor_{ℋ} B \land C \subseteq A \lor_{ℋ} B) \leftrightarrow (R \lor_{ℋ} A) \lor_{ℋ} C \subseteq A \lor_{ℋ} B$
46	43 45	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (R \lor_{ℋ} A) \lor_{ℋ} C \subseteq A \lor_{ℋ} B$
47	1 2 44 3	mdslj1i	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land (A \subseteq (R \lor_{ℋ} A) \cap C \land (R \lor_{ℋ} A) \lor_{ℋ} C \subseteq A \lor_{ℋ} B)) \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap B = ((R \lor_{ℋ} A) \cap B) \lor_{ℋ} (C \cap B)$
48	20 26 46 47	syl12anc	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap B = ((R \lor_{ℋ} A) \cap B) \lor_{ℋ} (C \cap B)$
49		simplll	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A 𝑀_{ℋ} B$
50		simplrl	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (A \subseteq C \land A \subseteq D)$
51		ssin	$⊢ (A \subseteq C \land A \subseteq D) \leftrightarrow A \subseteq C \cap D$
52	50 51	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \subseteq C \cap D$
53	52	ssrind	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \cap B \subseteq (C \cap D) \cap B$
54		inindir	$⊢ (C \cap D) \cap B = (C \cap B) \cap (D \cap B)$
55	53 54	sseqtrdi	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \cap B \subseteq (C \cap B) \cap (D \cap B)$
56		simprl	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (C \cap B) \cap (D \cap B) \subseteq R$
57	55 56	sstrd	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \cap B \subseteq R$
58		inss2	$⊢ D \cap B \subseteq B$
59		sstr	$⊢ (R \subseteq D \cap B \land D \cap B \subseteq B) \to R \subseteq B$
60	58 59	mpan2	$⊢ R \subseteq D \cap B \to R \subseteq B$
61	60	ad2antll	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to R \subseteq B$
62	1 2 5	3pm3.2i	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ} \land R \in C_{ℋ})$
63		mdsl3	$⊢ ((A \in C_{ℋ} \land B \in C_{ℋ} \land R \in C_{ℋ}) \land (A 𝑀_{ℋ} B \land A \cap B \subseteq R \land R \subseteq B)) \to (R \lor_{ℋ} A) \cap B = R$
64	62 63	mpan	$⊢ (A 𝑀_{ℋ} B \land A \cap B \subseteq R \land R \subseteq B) \to (R \lor_{ℋ} A) \cap B = R$
65	49 57 61 64	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (R \lor_{ℋ} A) \cap B = R$
66	65	oveq1d	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to ((R \lor_{ℋ} A) \cap B) \lor_{ℋ} (C \cap B) = R \lor_{ℋ} (C \cap B)$
67	48 66	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to R \lor_{ℋ} (C \cap B) = ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap B$
68	67	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (R \lor_{ℋ} (C \cap B)) \cap (D \cap B) = (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap B) \cap (D \cap B)$
69		inindir	$⊢ (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \cap B = (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap B) \cap (D \cap B)$
70	68 69	eqtr4di	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (R \lor_{ℋ} (C \cap B)) \cap (D \cap B) = (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \cap B$
71	52 23	jctil	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (A \subseteq R \lor_{ℋ} A \land A \subseteq C \cap D)$
72		ssin	$⊢ (A \subseteq R \lor_{ℋ} A \land A \subseteq C \cap D) \leftrightarrow A \subseteq (R \lor_{ℋ} A) \cap (C \cap D)$
73	71 72	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \subseteq (R \lor_{ℋ} A) \cap (C \cap D)$
74		ssinss1	$⊢ C \subseteq A \lor_{ℋ} B \to C \cap D \subseteq A \lor_{ℋ} B$
75	74	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$
76	75	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to C \cap D \subseteq A \lor_{ℋ} B$
77	40 76	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (R \lor_{ℋ} A \subseteq A \lor_{ℋ} B \land C \cap D \subseteq A \lor_{ℋ} B)$
78	3 4	chincli	$⊢ C \cap D \in C_{ℋ}$
79	44 78 38	chlubi	$⊢ (R \lor_{ℋ} A \subseteq A \lor_{ℋ} B \land C \cap D \subseteq A \lor_{ℋ} B) \leftrightarrow (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B$
80	77 79	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B$
81	1 2 44 78	mdslj1i	$⊢ ((A 𝑀_{ℋ} B \land B 𝑀_{ℋ}^{*} A) \land (A \subseteq (R \lor_{ℋ} A) \cap (C \cap D) \land (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B)) \to ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \cap B = ((R \lor_{ℋ} A) \cap B) \lor_{ℋ} ((C \cap D) \cap B)$
82	20 73 80 81	syl12anc	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \cap B = ((R \lor_{ℋ} A) \cap B) \lor_{ℋ} ((C \cap D) \cap B)$
83	54	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (C \cap D) \cap B = (C \cap B) \cap (D \cap B)$
84	65 83	oveq12d	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to ((R \lor_{ℋ} A) \cap B) \lor_{ℋ} ((C \cap D) \cap B) = R \lor_{ℋ} ((C \cap B) \cap (D \cap B))$
85	82 84	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to R \lor_{ℋ} ((C \cap B) \cap (D \cap B)) = ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \cap B$
86	70 85	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to ((R \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq R \lor_{ℋ} ((C \cap B) \cap (D \cap B)) \leftrightarrow (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \cap B \subseteq ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \cap B)$
87		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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to B 𝑀_{ℋ}^{} A$
88		simplr	$⊢ ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \to A \subseteq D$
89	88	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \subseteq D$
90	44 3	chub1i	$⊢ R \lor_{ℋ} A \subseteq (R \lor_{ℋ} A) \lor_{ℋ} C$
91	23 90	sstri	$⊢ A \subseteq (R \lor_{ℋ} A) \lor_{ℋ} C$
92	89 91	jctil	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (A \subseteq (R \lor_{ℋ} A) \lor_{ℋ} C \land A \subseteq D)$
93		ssin	$⊢ (A \subseteq (R \lor_{ℋ} A) \lor_{ℋ} C \land A \subseteq D) \leftrightarrow A \subseteq ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D$
94	92 93	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \subseteq ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D$
95	44 78	chub1i	$⊢ R \lor_{ℋ} A \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)$
96	23 95	sstri	$⊢ A \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)$
97	94 96	jctir	$⊢ (((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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (A \subseteq ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \land A \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D))$
98		ssin	$⊢ (A \subseteq ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \land A \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \leftrightarrow A \subseteq (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \cap ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D))$
99	97 98	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to A \subseteq (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \cap ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D))$
100		inss2	$⊢ ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq D$
101		sstr	$⊢ (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq D \land D \subseteq A \lor_{ℋ} B) \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B$
102	100 101	mpan	$⊢ D \subseteq A \lor_{ℋ} B \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B$
103	102	ad2antll	$⊢ ((A \subseteq C \land A \subseteq D) \land (C \subseteq A \lor_{ℋ} B \land D \subseteq A \lor_{ℋ} B)) \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B$
104	103	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B$
105	104 80	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B \land (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B)$
106	44 3	chjcli	$⊢ (R \lor_{ℋ} A) \lor_{ℋ} C \in C_{ℋ}$
107	106 4	chincli	$⊢ ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \in C_{ℋ}$
108	44 78	chjcli	$⊢ (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D) \in C_{ℋ}$
109	107 108 38	chlubi	$⊢ (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq A \lor_{ℋ} B \land (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D) \subseteq A \lor_{ℋ} B) \leftrightarrow (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \lor_{ℋ} ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \subseteq A \lor_{ℋ} B$
110	105 109	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \lor_{ℋ} ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \subseteq A \lor_{ℋ} B$
111	1 2 107 108	mdslle1i	$⊢ (B 𝑀_{ℋ}^{*} A \land A \subseteq (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \cap ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \land (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \lor_{ℋ} ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \subseteq A \lor_{ℋ} B) \to (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D) \leftrightarrow (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \cap B \subseteq ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \cap B)$
112	87 99 110 111	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D) \leftrightarrow (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D) \cap B \subseteq ((R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \cap B)$
113	86 112	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B)) \to ((R \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq R \lor_{ℋ} ((C \cap B) \cap (D \cap B)) \leftrightarrow ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D))$
114	113	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B) \to (((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D) \to (R \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq R \lor_{ℋ} ((C \cap B) \cap (D \cap B))))$
115	114	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 B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B) \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \to (((C \cap B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B) \to (R \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq R \lor_{ℋ} ((C \cap B) \cap (D \cap B))))$
116	19 115	syld	$⊢ ((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 \lor_{ℋ} A \subseteq D \to ((R \lor_{ℋ} A) \lor_{ℋ} C) \cap D \subseteq (R \lor_{ℋ} A) \lor_{ℋ} (C \cap D)) \to (((C \cap B) \cap (D \cap B) \subseteq R \land R \subseteq D \cap B) \to (R \lor_{ℋ} (C \cap B)) \cap (D \cap B) \subseteq R \lor_{ℋ} ((C \cap B) \cap (D \cap B))))$

Metamath Proof Explorer

Theorem mdslmd1lem1

Proof