# Metamath Proof Explorer

## Theorem mdslmd1lem3

Description: Lemma for mdslmd1i . (Contributed by NM, 29-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 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)$

### 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 oveq1 ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to {x}{\vee }_{ℋ}{A}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}$
6 5 sseq1d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}{A}\subseteq {D}↔if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\subseteq {D}\right)$
7 5 oveq1d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}=\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}$
8 7 ineq1d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}=\left(\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}$
9 5 oveq1d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)=\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)$
10 8 9 sseq12d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\left(\left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left({x}{\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)↔\left(\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)\right)$
11 6 10 imbi12d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\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)↔\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\subseteq {D}\to \left(\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}\left({C}\cap {D}\right)\right)\right)$
12 sseq2 ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq {x}↔\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\right)$
13 sseq1 ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left({x}\subseteq {D}\cap {B}↔if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {D}\cap {B}\right)$
14 12 13 anbi12d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq {x}\wedge {x}\subseteq {D}\cap {B}\right)↔\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\wedge if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {D}\cap {B}\right)\right)$
15 oveq1 ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to {x}{\vee }_{ℋ}\left({C}\cap {B}\right)=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left({C}\cap {B}\right)$
16 15 ineq1d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)=\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)$
17 oveq1 ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to {x}{\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)$
18 16 17 sseq12d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\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)↔\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)$
19 14 18 imbi12d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\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)↔\left(\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\wedge if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {D}\cap {B}\right)\to \left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
20 11 19 imbi12d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\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)↔\left(\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\subseteq {D}\to \left(\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\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 if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\wedge if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {D}\cap {B}\right)\to \left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)\right)$
21 20 imbi2d ${⊢}{x}=if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\to \left(\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(\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)\right)↔\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(\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\subseteq {D}\to \left(\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\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 if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\wedge if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {D}\cap {B}\right)\to \left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)\right)\right)$
22 h0elch ${⊢}{0}_{ℋ}\in {\mathbf{C}}_{ℋ}$
23 22 elimel ${⊢}if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\in {\mathbf{C}}_{ℋ}$
24 1 2 3 4 23 mdslmd1lem1 ${⊢}\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(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\subseteq {D}\to \left(\left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}{A}\right){\vee }_{ℋ}{C}\right)\cap {D}\subseteq \left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\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 if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\wedge if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right)\subseteq {D}\cap {B}\right)\to \left(if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left({C}\cap {B}\right)\right)\cap \left({D}\cap {B}\right)\subseteq if\left({x}\in {\mathbf{C}}_{ℋ},{x},{0}_{ℋ}\right){\vee }_{ℋ}\left(\left({C}\cap {B}\right)\cap \left({D}\cap {B}\right)\right)\right)\right)$
25 21 24 dedth ${⊢}{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(\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)\right)$
26 25 imp ${⊢}\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)$