# Metamath Proof Explorer

## Theorem dmdbr

Description: Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Assertion dmdbr ${⊢}\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({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}{y}={A}\to \left({y}\in {\mathbf{C}}_{ℋ}↔{A}\in {\mathbf{C}}_{ℋ}\right)$
2 1 anbi1d ${⊢}{y}={A}\to \left(\left({y}\in {\mathbf{C}}_{ℋ}\wedge {z}\in {\mathbf{C}}_{ℋ}\right)↔\left({A}\in {\mathbf{C}}_{ℋ}\wedge {z}\in {\mathbf{C}}_{ℋ}\right)\right)$
3 ineq2 ${⊢}{y}={A}\to {x}\cap {y}={x}\cap {A}$
4 3 oveq1d ${⊢}{y}={A}\to \left({x}\cap {y}\right){\vee }_{ℋ}{z}=\left({x}\cap {A}\right){\vee }_{ℋ}{z}$
5 oveq1 ${⊢}{y}={A}\to {y}{\vee }_{ℋ}{z}={A}{\vee }_{ℋ}{z}$
6 5 ineq2d ${⊢}{y}={A}\to {x}\cap \left({y}{\vee }_{ℋ}{z}\right)={x}\cap \left({A}{\vee }_{ℋ}{z}\right)$
7 4 6 eqeq12d ${⊢}{y}={A}\to \left(\left({x}\cap {y}\right){\vee }_{ℋ}{z}={x}\cap \left({y}{\vee }_{ℋ}{z}\right)↔\left({x}\cap {A}\right){\vee }_{ℋ}{z}={x}\cap \left({A}{\vee }_{ℋ}{z}\right)\right)$
8 7 imbi2d ${⊢}{y}={A}\to \left(\left({z}\subseteq {x}\to \left({x}\cap {y}\right){\vee }_{ℋ}{z}={x}\cap \left({y}{\vee }_{ℋ}{z}\right)\right)↔\left({z}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{z}={x}\cap \left({A}{\vee }_{ℋ}{z}\right)\right)\right)$
9 8 ralbidv ${⊢}{y}={A}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {x}\to \left({x}\cap {y}\right){\vee }_{ℋ}{z}={x}\cap \left({y}{\vee }_{ℋ}{z}\right)\right)↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{z}={x}\cap \left({A}{\vee }_{ℋ}{z}\right)\right)\right)$
10 2 9 anbi12d ${⊢}{y}={A}\to \left(\left(\left({y}\in {\mathbf{C}}_{ℋ}\wedge {z}\in {\mathbf{C}}_{ℋ}\right)\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {x}\to \left({x}\cap {y}\right){\vee }_{ℋ}{z}={x}\cap \left({y}{\vee }_{ℋ}{z}\right)\right)\right)↔\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {z}\in {\mathbf{C}}_{ℋ}\right)\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{z}={x}\cap \left({A}{\vee }_{ℋ}{z}\right)\right)\right)\right)$
11 eleq1 ${⊢}{z}={B}\to \left({z}\in {\mathbf{C}}_{ℋ}↔{B}\in {\mathbf{C}}_{ℋ}\right)$
12 11 anbi2d ${⊢}{z}={B}\to \left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {z}\in {\mathbf{C}}_{ℋ}\right)↔\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\right)$
13 sseq1 ${⊢}{z}={B}\to \left({z}\subseteq {x}↔{B}\subseteq {x}\right)$
14 oveq2 ${⊢}{z}={B}\to \left({x}\cap {A}\right){\vee }_{ℋ}{z}=\left({x}\cap {A}\right){\vee }_{ℋ}{B}$
15 oveq2 ${⊢}{z}={B}\to {A}{\vee }_{ℋ}{z}={A}{\vee }_{ℋ}{B}$
16 15 ineq2d ${⊢}{z}={B}\to {x}\cap \left({A}{\vee }_{ℋ}{z}\right)={x}\cap \left({A}{\vee }_{ℋ}{B}\right)$
17 14 16 eqeq12d ${⊢}{z}={B}\to \left(\left({x}\cap {A}\right){\vee }_{ℋ}{z}={x}\cap \left({A}{\vee }_{ℋ}{z}\right)↔\left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)$
18 13 17 imbi12d ${⊢}{z}={B}\to \left(\left({z}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{z}={x}\cap \left({A}{\vee }_{ℋ}{z}\right)\right)↔\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
19 18 ralbidv ${⊢}{z}={B}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{z}={x}\cap \left({A}{\vee }_{ℋ}{z}\right)\right)↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$
20 12 19 anbi12d ${⊢}{z}={B}\to \left(\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {z}\in {\mathbf{C}}_{ℋ}\right)\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{z}={x}\cap \left({A}{\vee }_{ℋ}{z}\right)\right)\right)↔\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\right)$
21 df-dmd ${⊢}{𝑀}_{ℋ}^{*}=\left\{⟨{y},{z}⟩|\left(\left({y}\in {\mathbf{C}}_{ℋ}\wedge {z}\in {\mathbf{C}}_{ℋ}\right)\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({z}\subseteq {x}\to \left({x}\cap {y}\right){\vee }_{ℋ}{z}={x}\cap \left({y}{\vee }_{ℋ}{z}\right)\right)\right)\right\}$
22 10 20 21 brabg ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}^{*}{B}↔\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\wedge \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)\right)$
23 22 bianabs ${⊢}\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({B}\subseteq {x}\to \left({x}\cap {A}\right){\vee }_{ℋ}{B}={x}\cap \left({A}{\vee }_{ℋ}{B}\right)\right)\right)$