This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mdslmd3i

Description: Modular pair conditions that imply the modular pair property in a sublattice. Lemma 1.5.1 of MaedaMaeda p. 2. (Contributed by NM, 23-Dec-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdslmd.1 ⊢ 𝐴 ∈ Cℋ
mdslmd.2 ⊢ 𝐵 ∈ Cℋ
mdslmd.3 ⊢ 𝐶 ∈ Cℋ
mdslmd.4 ⊢ 𝐷 ∈ Cℋ
Assertion mdslmd3i ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) → 𝐷 𝑀ℋ ( 𝐵 ∩ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mdslmd.1 ⊢ 𝐴 ∈ Cℋ
2 mdslmd.2 ⊢ 𝐵 ∈ Cℋ
3 mdslmd.3 ⊢ 𝐶 ∈ Cℋ
4 mdslmd.4 ⊢ 𝐷 ∈ Cℋ
5 chlej2 ⊢ ( ( ( 𝐷 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ 𝐷 ⊆ 𝐴 ) → ( 𝑥 ∨ℋ 𝐷 ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
6 5 ex ⊢ ( ( 𝐷 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( 𝐷 ⊆ 𝐴 → ( 𝑥 ∨ℋ 𝐷 ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) ) )
7 4 1 6 mp3an12 ⊢ ( 𝑥 ∈ Cℋ → ( 𝐷 ⊆ 𝐴 → ( 𝑥 ∨ℋ 𝐷 ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) ) )
8 7 impcom ⊢ ( ( 𝐷 ⊆ 𝐴 ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ∨ℋ 𝐷 ) ⊆ ( 𝑥 ∨ℋ 𝐴 ) )
9 8 ssrind ⊢ ( ( 𝐷 ⊆ 𝐴 ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐷 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) )
10 9 adantll ⊢ ( ( ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐷 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) )
11 10 adantll ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐷 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) )
12 11 adantr ⊢ ( ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ Cℋ ) ∧ 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) ) → ( ( 𝑥 ∨ℋ 𝐷 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) )
13 ssin ⊢ ( ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶 ) ↔ 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) )
14 inass ⊢ ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) )
15 mdi ⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
16 1 15 mp3anl1 ⊢ ( ( ( 𝐵 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
17 2 16 mpanl1 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) )
18 17 ineq1d ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∩ 𝐵 ) ∩ 𝐶 ) = ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) )
19 14 18 eqtr3id ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( 𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) )
20 19 adantrlr ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ 𝑥 ⊆ 𝐵 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) )
21 20 adantrrr ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶 ) ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) )
22 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
23 mdi ⊢ ( ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐶 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ∧ 𝑥 ⊆ 𝐶 ) ) → ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) )
24 22 23 mp3anl1 ⊢ ( ( ( 𝐶 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) ∧ ( ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ∧ 𝑥 ⊆ 𝐶 ) ) → ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) )
25 3 24 mpanl1 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ∧ 𝑥 ⊆ 𝐶 ) ) → ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) )
26 inass ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) = ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) )
27 26 oveq2i ⊢ ( 𝑥 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) )
28 25 27 eqtrdi ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ∧ 𝑥 ⊆ 𝐶 ) ) → ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
29 28 adantrll ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ 𝑥 ⊆ 𝐶 ) ) → ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
30 29 adantrrl ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶 ) ) ) → ( ( 𝑥 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐶 ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
31 21 30 eqtrd ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶 ) ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
32 31 ancoms ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶 ) ) ∧ 𝑥 ∈ Cℋ ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
33 32 an32s ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ 𝑥 ∈ Cℋ ) ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
34 13 33 sylan2br ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ 𝑥 ∈ Cℋ ) ∧ 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
35 34 adantllr ⊢ ( ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ Cℋ ) ∧ 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
36 inass ⊢ ( ( 𝐴 ∩ 𝐶 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐴 ∩ ( 𝐶 ∩ ( 𝐵 ∩ 𝐶 ) ) )
37 in12 ⊢ ( 𝐶 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐵 ∩ ( 𝐶 ∩ 𝐶 ) )
38 inidm ⊢ ( 𝐶 ∩ 𝐶 ) = 𝐶
39 38 ineq2i ⊢ ( 𝐵 ∩ ( 𝐶 ∩ 𝐶 ) ) = ( 𝐵 ∩ 𝐶 )
40 37 39 eqtri ⊢ ( 𝐶 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐵 ∩ 𝐶 )
41 40 ineq2i ⊢ ( 𝐴 ∩ ( 𝐶 ∩ ( 𝐵 ∩ 𝐶 ) ) ) = ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) )
42 36 41 eqtr2i ⊢ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( ( 𝐴 ∩ 𝐶 ) ∩ ( 𝐵 ∩ 𝐶 ) )
43 ssrin ⊢ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 → ( ( 𝐴 ∩ 𝐶 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) )
44 42 43 eqsstrid ⊢ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 → ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) )
45 ssrin ⊢ ( 𝐷 ⊆ 𝐴 → ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) )
46 44 45 anim12i ⊢ ( ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) → ( ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
47 eqss ⊢ ( ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ↔ ( ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ∧ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
48 46 47 sylibr ⊢ ( ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) → ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) )
49 48 oveq2d ⊢ ( ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) = ( 𝑥 ∨ℋ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
50 49 ad3antlr ⊢ ( ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ Cℋ ) ∧ 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) ) → ( 𝑥 ∨ℋ ( 𝐴 ∩ ( 𝐵 ∩ 𝐶 ) ) ) = ( 𝑥 ∨ℋ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
51 35 50 eqtrd ⊢ ( ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ Cℋ ) ∧ 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ∩ ( 𝐵 ∩ 𝐶 ) ) = ( 𝑥 ∨ℋ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
52 12 51 sseqtrd ⊢ ( ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ Cℋ ) ∧ 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) ) → ( ( 𝑥 ∨ℋ 𝐷 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ) )
53 52 ex ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) → ( ( 𝑥 ∨ℋ 𝐷 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ) ) )
54 53 ralrimiva ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) → ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) → ( ( 𝑥 ∨ℋ 𝐷 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ) ) )
55 2 3 chincli ⊢ ( 𝐵 ∩ 𝐶 ) ∈ Cℋ
56 mdbr2 ⊢ ( ( 𝐷 ∈ Cℋ ∧ ( 𝐵 ∩ 𝐶 ) ∈ Cℋ ) → ( 𝐷 𝑀ℋ ( 𝐵 ∩ 𝐶 ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) → ( ( 𝑥 ∨ℋ 𝐷 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ) ) ) )
57 4 55 56 mp2an ⊢ ( 𝐷 𝑀ℋ ( 𝐵 ∩ 𝐶 ) ↔ ∀ 𝑥 ∈ Cℋ ( 𝑥 ⊆ ( 𝐵 ∩ 𝐶 ) → ( ( 𝑥 ∨ℋ 𝐷 ) ∩ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( 𝑥 ∨ℋ ( 𝐷 ∩ ( 𝐵 ∩ 𝐶 ) ) ) ) )
58 54 57 sylibr ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) 𝑀ℋ 𝐶 ) ∧ ( ( 𝐴 ∩ 𝐶 ) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴 ) ) → 𝐷 𝑀ℋ ( 𝐵 ∩ 𝐶 ) )