Theorem mdbr

Description: Binary relation expressing <. A , B >. is a modular pair. Definition 1.1 of MaedaMaeda p. 1. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	mdbr	$$⊢\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(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap 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		oveq2	$$⊢y=A\to x{\vee }_{\mathscr{H}}y=x{\vee }_{\mathscr{H}}A$$
4	3	ineq1d	$$⊢y=A\to \left(x{\vee }_{\mathscr{H}}y\right)\cap z=\left(x{\vee }_{\mathscr{H}}A\right)\cap z$$
5		ineq1	$$⊢y=A\to y\cap z=A\cap z$$
6	5	oveq2d	$$⊢y=A\to x{\vee }_{\mathscr{H}}\left(y\cap z\right)=x{\vee }_{\mathscr{H}}\left(A\cap z\right)$$
7	4 6	eqeq12d	$$⊢y=A\to \left(\left(x{\vee }_{\mathscr{H}}y\right)\cap z=x{\vee }_{\mathscr{H}}\left(y\cap z\right)\leftrightarrow \left(x{\vee }_{\mathscr{H}}A\right)\cap z=x{\vee }_{\mathscr{H}}\left(A\cap z\right)\right)$$
8	7	imbi2d	$$⊢y=A\to \left(\left(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}y\right)\cap z=x{\vee }_{\mathscr{H}}\left(y\cap z\right)\right)\leftrightarrow \left(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}A\right)\cap z=x{\vee }_{\mathscr{H}}\left(A\cap z\right)\right)\right)$$
9	8	ralbidv	$$⊢y=A\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}y\right)\cap z=x{\vee }_{\mathscr{H}}\left(y\cap z\right)\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}A\right)\cap z=x{\vee }_{\mathscr{H}}\left(A\cap 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(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}y\right)\cap z=x{\vee }_{\mathscr{H}}\left(y\cap 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(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}A\right)\cap z=x{\vee }_{\mathscr{H}}\left(A\cap 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		sseq2	$$⊢z=B\to \left(x\subseteq z\leftrightarrow x\subseteq B\right)$$
14		ineq2	$$⊢z=B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap z=\left(x{\vee }_{\mathscr{H}}A\right)\cap B$$
15		ineq2	$$⊢z=B\to A\cap z=A\cap B$$
16	15	oveq2d	$$⊢z=B\to x{\vee }_{\mathscr{H}}\left(A\cap z\right)=x{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
17	14 16	eqeq12d	$$⊢z=B\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap z=x{\vee }_{\mathscr{H}}\left(A\cap z\right)\leftrightarrow \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
18	13 17	imbi12d	$$⊢z=B\to \left(\left(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}A\right)\cap z=x{\vee }_{\mathscr{H}}\left(A\cap z\right)\right)\leftrightarrow \left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
19	18	ralbidv	$$⊢z=B\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}A\right)\cap z=x{\vee }_{\mathscr{H}}\left(A\cap z\right)\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap 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(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}A\right)\cap z=x{\vee }_{\mathscr{H}}\left(A\cap 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(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)\right)$$
21		df-md	$$⊢{𝑀}_{\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(x\subseteq z\to \left(x{\vee }_{\mathscr{H}}y\right)\cap z=x{\vee }_{\mathscr{H}}\left(y\cap 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(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap 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(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$