# Metamath Proof Explorer

## Theorem mdi

Description: Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mdi ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}{𝑀}_{ℋ}{B}\wedge {C}\subseteq {B}\right)\right)\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}{\vee }_{ℋ}\left({A}\cap {B}\right)$

### Proof

Step Hyp Ref Expression
1 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)$
2 1 biimpd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}\to \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)$
3 sseq1 ${⊢}{x}={C}\to \left({x}\subseteq {B}↔{C}\subseteq {B}\right)$
4 oveq1 ${⊢}{x}={C}\to {x}{\vee }_{ℋ}{A}={C}{\vee }_{ℋ}{A}$
5 4 ineq1d ${⊢}{x}={C}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}=\left({C}{\vee }_{ℋ}{A}\right)\cap {B}$
6 oveq1 ${⊢}{x}={C}\to {x}{\vee }_{ℋ}\left({A}\cap {B}\right)={C}{\vee }_{ℋ}\left({A}\cap {B}\right)$
7 5 6 eqeq12d ${⊢}{x}={C}\to \left(\left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)↔\left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
8 3 7 imbi12d ${⊢}{x}={C}\to \left(\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)↔\left({C}\subseteq {B}\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
9 8 rspcv ${⊢}{C}\in {\mathbf{C}}_{ℋ}\to \left(\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 \left({C}\subseteq {B}\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
10 2 9 sylan9 ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}\to \left({C}\subseteq {B}\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
11 10 3impa ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}\to \left({C}\subseteq {B}\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
12 11 imp32 ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left({A}{𝑀}_{ℋ}{B}\wedge {C}\subseteq {B}\right)\right)\to \left({C}{\vee }_{ℋ}{A}\right)\cap {B}={C}{\vee }_{ℋ}\left({A}\cap {B}\right)$