Theorem mdslj1i

Description: Join preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslle1.1	⊢ 𝐴 ∈ Cℋ
	mdslle1.2	⊢ 𝐵 ∈ Cℋ
	mdslle1.3	⊢ 𝐶 ∈ Cℋ
	mdslle1.4	⊢ 𝐷 ∈ Cℋ
Assertion	mdslj1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdslle1.1	⊢ 𝐴 ∈ Cℋ
2		mdslle1.2	⊢ 𝐵 ∈ Cℋ
3		mdslle1.3	⊢ 𝐶 ∈ Cℋ
4		mdslle1.4	⊢ 𝐷 ∈ Cℋ
5		ssin	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ↔ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
6	5	bicomi	⊢ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ↔ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) )
7	1 2	chjcli	⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
8	3 4 7	chlubi	⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
9	8	bicomi	⊢ ( ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ↔ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
10	6 9	anbi12i	⊢ ( ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
11		simpr	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) → 𝐵 𝑀ℋ* 𝐴 )
12		simpl	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → 𝐴 ⊆ 𝐶 )
13		simpl	⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
14	1 2 3	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ )
15		dmdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐶 )
16	14 15	mpan	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐶 )
17	11 12 13 16	syl3an	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐶 )
18	3 2	chincli	⊢ ( 𝐶 ∩ 𝐵 ) ∈ Cℋ
19	4 2	chincli	⊢ ( 𝐷 ∩ 𝐵 ) ∈ Cℋ
20	18 19	chub1i	⊢ ( 𝐶 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) )
21	18 19	chjcli	⊢ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∈ Cℋ
22	18 21 1	chlej1i	⊢ ( ( 𝐶 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
23	20 22	mp1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
24	17 23	eqsstrrd	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐶 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
25		simpr	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → 𝐴 ⊆ 𝐷 )
26		simpr	⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
27	1 2 4	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )
28		dmdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) ∧ ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
29	27 28	mpan	⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
30	11 25 26 29	syl3an	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) = 𝐷 )
31	19 18	chub2i	⊢ ( 𝐷 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) )
32	19 21 1	chlej1i	⊢ ( ( 𝐷 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
33	31 32	mp1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐷 ∩ 𝐵 ) ∨ℋ 𝐴 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
34	30 33	eqsstrrd	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐷 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
35	24 34	jca	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∧ 𝐷 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ) )
36	21 1	chjcli	⊢ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∈ Cℋ
37	3 4 36	chlubi	⊢ ( ( 𝐶 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∧ 𝐷 ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ) ↔ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
38	35 37	sylib	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) )
39	38	ssrind	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) )
40		simpl	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) → 𝐴 𝑀ℋ 𝐵 )
41		ssrin	⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐵 ) )
42	41 20	sstrdi	⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
43	42	adantr	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
44		inss2	⊢ ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵
45		inss2	⊢ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐵
46	18 19 2	chlubi	⊢ ( ( ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐵 ) ↔ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 )
47	46	bicomi	⊢ ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 ↔ ( ( 𝐶 ∩ 𝐵 ) ⊆ 𝐵 ∧ ( 𝐷 ∩ 𝐵 ) ⊆ 𝐵 ) )
48	44 45 47	mpbir2an	⊢ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵
49	48	a1i	⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 )
50	1 2 21	3pm3.2i	⊢ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∈ Cℋ )
51		mdsl3	⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∧ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
52	50 51	mpan	⊢ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∧ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝐵 ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
53	40 43 49 52	syl3an	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
54	39 53	sseqtrd	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
55	54	3expb	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
56	10 55	sylan2b	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )
57	3 4 2	lediri	⊢ ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 )
58	57	a1i	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) )
59	56 58	eqssd	⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝐶 ∨ℋ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∨ℋ ( 𝐷 ∩ 𝐵 ) ) )