# Metamath Proof Explorer

## Theorem mddmd2

Description: Relationship between modular pairs and dual-modular pairs. Lemma 1.2 of MaedaMaeda p. 1. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion mddmd2 ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{x}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}^{*}{x}\right)$

### Proof

Step Hyp Ref Expression
1 breq2 ${⊢}{x}={y}\to \left({A}{𝑀}_{ℋ}{x}↔{A}{𝑀}_{ℋ}{y}\right)$
2 1 cbvralvw ${⊢}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{x}↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{y}$
3 mdbr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{y}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {y}={x}{\vee }_{ℋ}\left({A}\cap {y}\right)\right)\right)$
4 incom ${⊢}\left({A}{\vee }_{ℋ}{x}\right)\cap {y}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)$
5 chjcom ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {A}{\vee }_{ℋ}{x}={x}{\vee }_{ℋ}{A}$
6 5 ineq1d ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{\vee }_{ℋ}{x}\right)\cap {y}=\left({x}{\vee }_{ℋ}{A}\right)\cap {y}$
7 4 6 syl5reqr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}{A}\right)\cap {y}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)$
8 7 adantlr ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}{A}\right)\cap {y}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)$
9 incom ${⊢}{A}\cap {y}={y}\cap {A}$
10 9 oveq1i ${⊢}\left({A}\cap {y}\right){\vee }_{ℋ}{x}=\left({y}\cap {A}\right){\vee }_{ℋ}{x}$
11 chincl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to {A}\cap {y}\in {\mathbf{C}}_{ℋ}$
12 chjcom ${⊢}\left({A}\cap {y}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\cap {y}\right){\vee }_{ℋ}{x}={x}{\vee }_{ℋ}\left({A}\cap {y}\right)$
13 11 12 sylan ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\cap {y}\right){\vee }_{ℋ}{x}={x}{\vee }_{ℋ}\left({A}\cap {y}\right)$
14 10 13 syl5reqr ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {x}{\vee }_{ℋ}\left({A}\cap {y}\right)=\left({y}\cap {A}\right){\vee }_{ℋ}{x}$
15 8 14 eqeq12d ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({x}{\vee }_{ℋ}{A}\right)\cap {y}={x}{\vee }_{ℋ}\left({A}\cap {y}\right)↔{y}\cap \left({A}{\vee }_{ℋ}{x}\right)=\left({y}\cap {A}\right){\vee }_{ℋ}{x}\right)$
16 eqcom ${⊢}{y}\cap \left({A}{\vee }_{ℋ}{x}\right)=\left({y}\cap {A}\right){\vee }_{ℋ}{x}↔\left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)$
17 15 16 syl6bb ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({x}{\vee }_{ℋ}{A}\right)\cap {y}={x}{\vee }_{ℋ}\left({A}\cap {y}\right)↔\left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)$
18 17 imbi2d ${⊢}\left(\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({x}\subseteq {y}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {y}={x}{\vee }_{ℋ}\left({A}\cap {y}\right)\right)↔\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)\right)$
19 18 ralbidva ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {y}={x}{\vee }_{ℋ}\left({A}\cap {y}\right)\right)↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)\right)$
20 3 19 bitrd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {y}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{y}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)\right)$
21 20 ralbidva ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left(\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{y}↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)\right)$
22 2 21 syl5bb ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{x}↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)\right)$
23 ralcom ${⊢}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)$
24 22 23 syl6bb ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{x}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)\right)$
25 dmdbr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}^{*}{x}↔\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)\right)$
26 25 ralbidva ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}^{*}{x}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {y}\to \left({y}\cap {A}\right){\vee }_{ℋ}{x}={y}\cap \left({A}{\vee }_{ℋ}{x}\right)\right)\right)$
27 24 26 bitr4d ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left(\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}{x}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}{A}{𝑀}_{ℋ}^{*}{x}\right)$