# Metamath Proof Explorer

## Theorem mdslmd1i

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

Ref Expression
Hypotheses mdslmd.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
mdslmd.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
mdslmd.3 ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
mdslmd.4 ${⊢}{D}\in {\mathbf{C}}_{ℋ}$
Assertion mdslmd1i ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left({A}\subseteq {C}\cap {D}\wedge {C}{\vee }_{ℋ}{D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\to \left({C}{𝑀}_{ℋ}{D}↔\left({C}\cap {B}\right){𝑀}_{ℋ}\left({D}\cap {B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 mdslmd.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 mdslmd.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 mdslmd.3 ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
4 mdslmd.4 ${⊢}{D}\in {\mathbf{C}}_{ℋ}$
5 ssin ${⊢}\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)↔{A}\subseteq {C}\cap {D}$
6 1 2 chjcli ${⊢}{A}{\vee }_{ℋ}{B}\in {\mathbf{C}}_{ℋ}$
7 3 4 6 chlubi ${⊢}\left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)↔{C}{\vee }_{ℋ}{D}\subseteq {A}{\vee }_{ℋ}{B}$
8 5 7 anbi12i ${⊢}\left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)↔\left({A}\subseteq {C}\cap {D}\wedge {C}{\vee }_{ℋ}{D}\subseteq {A}{\vee }_{ℋ}{B}\right)$
9 chjcl ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to {x}{\vee }_{ℋ}{A}\in {\mathbf{C}}_{ℋ}$
10 1 9 mpan2 ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to {x}{\vee }_{ℋ}{A}\in {\mathbf{C}}_{ℋ}$
11 sseq1 ${⊢}{y}={x}{\vee }_{ℋ}{A}\to \left({y}\subseteq {D}↔{x}{\vee }_{ℋ}{A}\subseteq {D}\right)$
12 oveq1 ${⊢}{y}={x}{\vee }_{ℋ}{A}\to {y}{\vee }_{ℋ}{C}=\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}$
13 12 ineq1d ${⊢}{y}={x}{\vee }_{ℋ}{A}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}=\left(\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}$
14 oveq1 ${⊢}{y}={x}{\vee }_{ℋ}{A}\to {y}{\vee }_{ℋ}\left({C}\cap {D}\right)=\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)$
15 13 14 sseq12d ${⊢}{y}={x}{\vee }_{ℋ}{A}\to \left(\left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)↔\left(\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)\right)$
16 11 15 imbi12d ${⊢}{y}={x}{\vee }_{ℋ}{A}\to \left(\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)↔\left({x}{\vee }_{ℋ}{A}\subseteq {D}\to \left(\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)$
17 16 rspcv ${⊢}{x}{\vee }_{ℋ}{A}\in {\mathbf{C}}_{ℋ}\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\to \left({x}{\vee }_{ℋ}{A}\subseteq {D}\to \left(\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)$
18 10 17 syl ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\to \left({x}{\vee }_{ℋ}{A}\subseteq {D}\to \left(\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)$
19 18 adantr ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\to \left({x}{\vee }_{ℋ}{A}\subseteq {D}\to \left(\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)$
20 1 2 3 4 mdslmd1lem3 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\right)\to \left(\left({x}{\vee }_{ℋ}{A}\subseteq {D}\to \left(\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)\right)\to \left(\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq {x}\wedge {x}\subseteq {D}\cap {B}\right)\to \left({x}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {x}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
21 19 20 syld ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\to \left(\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq {x}\wedge {x}\subseteq {D}\cap {B}\right)\to \left({x}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {x}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
22 21 ex ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left(\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\to \left(\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq {x}\wedge {x}\subseteq {D}\cap {B}\right)\to \left({x}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {x}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)\right)$
23 22 com3l ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\to \left(\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq {x}\wedge {x}\subseteq {D}\cap {B}\right)\to \left({x}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {x}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)\right)$
24 23 ralrimdv ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq {x}\wedge {x}\subseteq {D}\cap {B}\right)\to \left({x}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {x}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
25 mdbr2 ${⊢}\left({C}\in {\mathbf{C}}_{ℋ}\wedge {D}\in {\mathbf{C}}_{ℋ}\right)\to \left({C}{𝑀}_{ℋ}{D}↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)$
26 3 4 25 mp2an ${⊢}{C}{𝑀}_{ℋ}{D}↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\to \left({y}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {y}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)$
27 3 2 chincli ${⊢}{C}\cap {B}\in {\mathbf{C}}_{ℋ}$
28 4 2 chincli ${⊢}{D}\cap {B}\in {\mathbf{C}}_{ℋ}$
29 27 28 mdsl2i ${⊢}\left({C}\cap {B}\right){𝑀}_{ℋ}\left({D}\cap {B}\right)↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq {x}\wedge {x}\subseteq {D}\cap {B}\right)\to \left({x}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {x}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)$
30 24 26 29 3imtr4g ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left({C}{𝑀}_{ℋ}{D}\to \left({C}\cap {B}\right){𝑀}_{ℋ}\left({D}\cap {B}\right)\right)$
31 chincl ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {x}\cap {B}\in {\mathbf{C}}_{ℋ}$
32 2 31 mpan2 ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to {x}\cap {B}\in {\mathbf{C}}_{ℋ}$
33 sseq1 ${⊢}{y}={x}\cap {B}\to \left({y}\subseteq {D}\cap {B}↔{x}\cap {B}\subseteq {D}\cap {B}\right)$
34 oveq1 ${⊢}{y}={x}\cap {B}\to {y}{\vee }_{ℋ}\left({C}\cap {B}\right)=\left({x}\cap {B}\right){\vee }_{ℋ}\left({C}\cap {B}\right)$
35 34 ineq1d ${⊢}{y}={x}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)=\left(\left({x}\cap {B}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)$
36 oveq1 ${⊢}{y}={x}\cap {B}\to {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)=\left({x}\cap {B}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)$
37 35 36 sseq12d ${⊢}{y}={x}\cap {B}\to \left(\left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)↔\left(\left({x}\cap {B}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq \left({x}\cap {B}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)$
38 33 37 imbi12d ${⊢}{y}={x}\cap {B}\to \left(\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)↔\left({x}\cap {B}\subseteq {D}\cap {B}\to \left(\left({x}\cap {B}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq \left({x}\cap {B}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
39 38 rspcv ${⊢}{x}\cap {B}\in {\mathbf{C}}_{ℋ}\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\to \left({x}\cap {B}\subseteq {D}\cap {B}\to \left(\left({x}\cap {B}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq \left({x}\cap {B}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
40 32 39 syl ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\to \left({x}\cap {B}\subseteq {D}\cap {B}\to \left(\left({x}\cap {B}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq \left({x}\cap {B}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
41 40 adantr ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\to \left({x}\cap {B}\subseteq {D}\cap {B}\to \left(\left({x}\cap {B}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq \left({x}\cap {B}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
42 1 2 3 4 mdslmd1lem4 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\right)\to \left(\left({x}\cap {B}\subseteq {D}\cap {B}\to \left(\left({x}\cap {B}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq \left({x}\cap {B}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\to \left(\left({C}\cap {D}\subseteq {x}\wedge {x}\subseteq {D}\right)\to \left({x}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {x}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)$
43 41 42 syld ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge \left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\to \left(\left({C}\cap {D}\subseteq {x}\wedge {x}\subseteq {D}\right)\to \left({x}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {x}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)$
44 43 ex ${⊢}{x}\in {\mathbf{C}}_{ℋ}\to \left(\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\to \left(\left({C}\cap {D}\subseteq {x}\wedge {x}\subseteq {D}\right)\to \left({x}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {x}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)\right)$
45 44 com3l ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\to \left(\left({C}\cap {D}\subseteq {x}\wedge {x}\subseteq {D}\right)\to \left({x}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {x}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)\right)$
46 45 ralrimdv ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({C}\cap {D}\subseteq {x}\wedge {x}\subseteq {D}\right)\to \left({x}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {x}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)$
47 mdbr2 ${⊢}\left({C}\cap {B}\in {\mathbf{C}}_{ℋ}\wedge {D}\cap {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({C}\cap {B}\right){𝑀}_{ℋ}\left({D}\cap {B}\right)↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
48 27 28 47 mp2an ${⊢}\left({C}\cap {B}\right){𝑀}_{ℋ}\left({D}\cap {B}\right)↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {D}\cap {B}\to \left({y}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq {y}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)$
49 3 4 mdsl2i ${⊢}{C}{𝑀}_{ℋ}{D}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({C}\cap {D}\subseteq {x}\wedge {x}\subseteq {D}\right)\to \left({x}{\vee }_{ℋ}{C}\right)\cap {D}\subseteq {x}{\vee }_{ℋ}\left({C}\cap {D}\right)\right)$
50 46 48 49 3imtr4g ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left(\left({C}\cap {B}\right){𝑀}_{ℋ}\left({D}\cap {B}\right)\to {C}{𝑀}_{ℋ}{D}\right)$
51 30 50 impbid ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left(\left({A}\subseteq {C}\wedge {A}\subseteq {D}\right)\wedge \left({C}\subseteq {A}{\vee }_{ℋ}{B}\wedge {D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)\to \left({C}{𝑀}_{ℋ}{D}↔\left({C}\cap {B}\right){𝑀}_{ℋ}\left({D}\cap {B}\right)\right)$
52 8 51 sylan2br ${⊢}\left(\left({A}{𝑀}_{ℋ}{B}\wedge {B}{𝑀}_{ℋ}^{*}{A}\right)\wedge \left({A}\subseteq {C}\cap {D}\wedge {C}{\vee }_{ℋ}{D}\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\to \left({C}{𝑀}_{ℋ}{D}↔\left({C}\cap {B}\right){𝑀}_{ℋ}\left({D}\cap {B}\right)\right)$