# Metamath Proof Explorer

## Theorem mdsl1i

Description: If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdsl.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
mdsl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion mdsl1i ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)↔{A}{𝑀}_{ℋ}{B}$

### Proof

Step Hyp Ref Expression
1 mdsl.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 mdsl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 sseq2 ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to \left({A}\cap {B}\subseteq {x}↔{A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
4 sseq1 ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to \left({x}\subseteq {A}{\vee }_{ℋ}{B}↔{y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)$
5 3 4 anbi12d ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to \left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)↔\left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\right)$
6 sseq1 ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to \left({x}\subseteq {B}↔{y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\right)$
7 oveq1 ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to {x}{\vee }_{ℋ}{A}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}$
8 7 ineq1d ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}=\left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}$
9 oveq1 ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to {x}{\vee }_{ℋ}\left({A}\cap {B}\right)=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)$
10 8 9 eqeq12d ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to \left(\left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)↔\left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
11 6 10 imbi12d ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to \left(\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)↔\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
12 5 11 imbi12d ${⊢}{x}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\to \left(\left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)↔\left(\left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)\right)$
13 12 rspccv ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\to \left(\left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)\right)$
14 impexp ${⊢}\left(\left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\wedge \left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\right)\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)↔\left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\wedge \left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
15 impexp ${⊢}\left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\wedge \left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)↔\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\to \left(\left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)\right)$
16 14 15 bitr2i ${⊢}\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\to \left(\left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)\right)↔\left(\left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\wedge \left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\right)\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
17 inss2 ${⊢}{A}\cap {B}\subseteq {B}$
18 1 2 chincli ${⊢}{A}\cap {B}\in {\mathbf{C}}_{ℋ}$
19 chlub ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\cap {B}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({y}\subseteq {B}\wedge {A}\cap {B}\subseteq {B}\right)↔{y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\right)$
20 18 2 19 mp3an23 ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left(\left({y}\subseteq {B}\wedge {A}\cap {B}\subseteq {B}\right)↔{y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\right)$
21 20 biimpd ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left(\left({y}\subseteq {B}\wedge {A}\cap {B}\subseteq {B}\right)\to {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\right)$
22 17 21 mpan2i ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left({y}\subseteq {B}\to {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\right)$
23 2 1 chub2i ${⊢}{B}\subseteq {A}{\vee }_{ℋ}{B}$
24 sstr ${⊢}\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\wedge {B}\subseteq {A}{\vee }_{ℋ}{B}\right)\to {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}$
25 23 24 mpan2 ${⊢}{y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\to {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}$
26 22 25 syl6 ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left({y}\subseteq {B}\to {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)$
27 chub2 ${⊢}\left({A}\cap {B}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)$
28 18 27 mpan ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to {A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)$
29 26 28 jctild ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left({y}\subseteq {B}\to \left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\right)$
30 chjcl ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\cap {B}\in {\mathbf{C}}_{ℋ}\right)\to {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}$
31 18 30 mpan2 ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}$
32 29 31 jctild ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left({y}\subseteq {B}\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\wedge \left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\right)$
33 32 22 jcad ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left({y}\subseteq {B}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\wedge \left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\right)\right)$
34 chjass ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\cap {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}={y}{\vee }_{ℋ}\left(\left({A}\cap {B}\right){\vee }_{ℋ}{A}\right)$
35 18 1 34 mp3an23 ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}={y}{\vee }_{ℋ}\left(\left({A}\cap {B}\right){\vee }_{ℋ}{A}\right)$
36 18 1 chjcomi ${⊢}\left({A}\cap {B}\right){\vee }_{ℋ}{A}={A}{\vee }_{ℋ}\left({A}\cap {B}\right)$
37 1 2 chabs1i ${⊢}{A}{\vee }_{ℋ}\left({A}\cap {B}\right)={A}$
38 36 37 eqtri ${⊢}\left({A}\cap {B}\right){\vee }_{ℋ}{A}={A}$
39 38 oveq2i ${⊢}{y}{\vee }_{ℋ}\left(\left({A}\cap {B}\right){\vee }_{ℋ}{A}\right)={y}{\vee }_{ℋ}{A}$
40 35 39 syl6eq ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}={y}{\vee }_{ℋ}{A}$
41 40 ineq1d ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}{A}\right)\cap {B}$
42 chjass ${⊢}\left({y}\in {\mathbf{C}}_{ℋ}\wedge {A}\cap {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\cap {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)={y}{\vee }_{ℋ}\left(\left({A}\cap {B}\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
43 18 18 42 mp3an23 ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)={y}{\vee }_{ℋ}\left(\left({A}\cap {B}\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
44 18 chjidmi ${⊢}\left({A}\cap {B}\right){\vee }_{ℋ}\left({A}\cap {B}\right)={A}\cap {B}$
45 44 oveq2i ${⊢}{y}{\vee }_{ℋ}\left(\left({A}\cap {B}\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)={y}{\vee }_{ℋ}\left({A}\cap {B}\right)$
46 43 45 syl6eq ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)={y}{\vee }_{ℋ}\left({A}\cap {B}\right)$
47 41 46 eqeq12d ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left(\left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)↔\left({y}{\vee }_{ℋ}{A}\right)\cap {B}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
48 47 biimpd ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left(\left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\to \left({y}{\vee }_{ℋ}{A}\right)\cap {B}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
49 33 48 imim12d ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left(\left(\left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\wedge \left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\right)\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)\to \left({y}\subseteq {B}\to \left({y}{\vee }_{ℋ}{A}\right)\cap {B}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
50 16 49 syl5bi ${⊢}{y}\in {\mathbf{C}}_{ℋ}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\in {\mathbf{C}}_{ℋ}\to \left(\left({A}\cap {B}\subseteq {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\wedge {y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\subseteq {B}\to \left(\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}{A}\right)\cap {B}=\left({y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right){\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)\right)\to \left({y}\subseteq {B}\to \left({y}{\vee }_{ℋ}{A}\right)\cap {B}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
51 13 50 syl5com ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)\to \left({y}\in {\mathbf{C}}_{ℋ}\to \left({y}\subseteq {B}\to \left({y}{\vee }_{ℋ}{A}\right)\cap {B}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
52 51 ralrimiv ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)\to \forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {B}\to \left({y}{\vee }_{ℋ}{A}\right)\cap {B}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
53 mdbr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {B}\to \left({y}{\vee }_{ℋ}{A}\right)\cap {B}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
54 1 2 53 mp2an ${⊢}{A}{𝑀}_{ℋ}{B}↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({y}\subseteq {B}\to \left({y}{\vee }_{ℋ}{A}\right)\cap {B}={y}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
55 52 54 sylibr ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)\to {A}{𝑀}_{ℋ}{B}$
56 mdbr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
57 1 2 56 mp2an ${⊢}{A}{𝑀}_{ℋ}{B}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
58 ax-1 ${⊢}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\to \left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
59 58 ralimi ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
60 57 59 sylbi ${⊢}{A}{𝑀}_{ℋ}{B}\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
61 55 60 impbii ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left(\left({A}\cap {B}\subseteq {x}\wedge {x}\subseteq {A}{\vee }_{ℋ}{B}\right)\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)↔{A}{𝑀}_{ℋ}{B}$