Theorem dmdbr4

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

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

Proof

Step	Hyp	Ref	Expression
1		dmdbr2	$$⊢\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 y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\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 \left(A{\vee }_{\mathscr{H}}B\right)=\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
7		ineq1	$$⊢y=x{\vee }_{\mathscr{H}}B\to y\cap A=\left(x{\vee }_{\mathscr{H}}B\right)\cap A$$
8	7	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$$
9	6 8	sseq12d	$$⊢y=x{\vee }_{\mathscr{H}}B\to \left(y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$
10	5 9	imbi12d	$$⊢y=x{\vee }_{\mathscr{H}}B\to \left(\left(B\subseteq y\to y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(B\subseteq x{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\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 y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\to \left(B\subseteq x{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\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 y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\to \left(B\subseteq x{\vee }_{\mathscr{H}}B\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\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 y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\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 y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\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 y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\to \left(x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\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 y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\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 \left(A{\vee }_{\mathscr{H}}B\right)=x\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
20	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$$
21	20	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$$
22	19 21	sseq12d	$$⊢\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 \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow x\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(x\cap A\right){\vee }_{\mathscr{H}}B\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(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to x\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(x\cap A\right){\vee }_{\mathscr{H}}B\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(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to x\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(x\cap A\right){\vee }_{\mathscr{H}}B\right)\right)$$
25	24	com23	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \left(B\subseteq x\to x\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(x\cap A\right){\vee }_{\mathscr{H}}B\right)\right)$$
26	25	ralimdva	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq x\to x\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(x\cap A\right){\vee }_{\mathscr{H}}B\right)\right)$$
27		sseq2	$$⊢x=y\to \left(B\subseteq x\leftrightarrow B\subseteq y\right)$$
28		ineq1	$$⊢x=y\to x\cap \left(A{\vee }_{\mathscr{H}}B\right)=y\cap \left(A{\vee }_{\mathscr{H}}B\right)$$
29		ineq1	$$⊢x=y\to x\cap A=y\cap A$$
30	29	oveq1d	$$⊢x=y\to \left(x\cap A\right){\vee }_{\mathscr{H}}B=\left(y\cap A\right){\vee }_{\mathscr{H}}B$$
31	28 30	sseq12d	$$⊢x=y\to \left(x\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(x\cap A\right){\vee }_{\mathscr{H}}B\leftrightarrow y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)$$
32	27 31	imbi12d	$$⊢x=y\to \left(\left(B\subseteq x\to x\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(x\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \left(B\subseteq y\to y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\right)$$
33	32	cbvralvw	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq x\to x\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(x\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)$$
34	26 33	imbitrdi	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\to \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(B\subseteq y\to y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\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 y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\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 y\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(y\cap A\right){\vee }_{\mathscr{H}}B\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\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(x{\vee }_{\mathscr{H}}B\right)\cap \left(A{\vee }_{\mathscr{H}}B\right)\subseteq \left(\left(x{\vee }_{\mathscr{H}}B\right)\cap A\right){\vee }_{\mathscr{H}}B\right)$$