Theorem dmdbr3

Description: Binary relation expressing the dual modular pair property. This version quantifies an equality instead of an inference. (Contributed by NM, 6-Jul-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	dmdbr3	$$⊢\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(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dmdbr	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{𝑀}_{\mathscr{H}}^{*}B\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
2		chub2	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to B\subseteq x{\vee }_{\mathscr{H}}B$$
3	2	ancoms	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to B\subseteq x{\vee }_{\mathscr{H}}B$$
4		chjcl	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}$$
5		sseq2	$$⊢y=x{\vee }_{\mathscr{H}}B\to \left(B\subseteq y\leftrightarrow B\subseteq x{\vee }_{\mathscr{H}}B\right)$$
6		ineq1	$$⊢y=x{\vee }_{\mathscr{H}}B\to y\cap A=\left(x{\vee }_{\mathscr{H}}B\right)\cap A$$
7	6	oveq1d	$$⊢y=x{\vee }_{\mathscr{H}}B\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B$$
8		ineq1	$$⊢y=x{\vee }_{\mathscr{H}}B\to y\cap \left(A{\vee }_{\mathscr{H}}B\right)=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
9	7 8	eqeq12d	$$⊢y=x{\vee }_{\mathscr{H}}B\to \left(\left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
10	5 9	imbi12d	$$⊢y=x{\vee }_{\mathscr{H}}B\to \left(\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \left(B\subseteq x{\vee }_{\mathscr{H}}B\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
11	10	rspcv	$$⊢x{\vee }_{\mathscr{H}}B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\to \left(B\subseteq x{\vee }_{\mathscr{H}}B\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
12	4 11	syl	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\to \left(B\subseteq x{\vee }_{\mathscr{H}}B\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
13	3 12	mpid	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
14	13	ex	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
15	14	com3l	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\to \left(x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
16	15	ralrimdv	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
17		chlejb2	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B\subseteq x\leftrightarrow x{\vee }_{\mathscr{H}}B=x\right)$$
18	17	biimpa	$$⊢\left(\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge B\subseteq x\right)\to x{\vee }_{\mathscr{H}}B=x$$
19	18	ineq1d	$$⊢\left(\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge B\subseteq x\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap A=x\cap A$$
20	19	oveq1d	$$⊢\left(\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge B\subseteq x\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x\cap A\right){\vee }_{\mathscr{H}}B$$
21	18	ineq1d	$$⊢\left(\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge B\subseteq x\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)=x\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
22	20 21	eqeq12d	$$⊢\left(\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge B\subseteq x\right)\to \left(\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
23	22	biimpd	$$⊢\left(\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge B\subseteq x\right)\to \left(\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
24	23	ex	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B\subseteq x\to \left(\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
25	24	com23	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\to \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)$$
26	25	ralimdva	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\to \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)$$
27		sseq2	$$⊢x=y\to \left(B\subseteq x\leftrightarrow B\subseteq y\right)$$
28		ineq1	$$⊢x=y\to x\cap A=y\cap A$$
29	28	oveq1d	$$⊢x=y\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=\left(y\cap A\right){\vee }_{\mathscr{H}}B$$
30		ineq1	$$⊢x=y\to x\cap \left(A{\vee }_{\mathscr{H}}B\right)=y\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
31	29 30	eqeq12d	$$⊢x=y\to \left(\left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
32	27 31	imbi12d	$$⊢x=y\to \left(\left(B\subseteq x\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=x\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
33	32	cbvralvw	$$⊢\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)\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
34	26 33	imbitrdi	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\to \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\right)$$
35	16 34	impbid	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
36	35	adantl	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to \left(y\cap A\right){\vee }_{\mathscr{H}}B=y\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$
37	1 36	bitrd	$$⊢\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(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\right)$$