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}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}^{*}B\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq x\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$

Proof

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