Theorem mdbr4

Description: Binary relation expressing the 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	mdbr4	$$⊢\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\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdbr2	$$⊢\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(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
2		chincl	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to x\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
3		inss2	$$⊢x\cap B\subseteq B$$
4		sseq1	$$⊢y=x\cap B\to \left(y\subseteq B\leftrightarrow x\cap B\subseteq B\right)$$
5		oveq1	$$⊢y=x\cap B\to y{\vee }_{\mathscr{H}}A=\left(x\cap B\right){\vee }_{\mathscr{H}}A$$
6	5	ineq1d	$$⊢y=x\cap B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B=\left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B$$
7		oveq1	$$⊢y=x\cap B\to y{\vee }_{\mathscr{H}}\left(A\cap B\right)=\left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$
8	6 7	sseq12d	$$⊢y=x\cap B\to \left(\left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\leftrightarrow \left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
9	4 8	imbi12d	$$⊢y=x\cap B\to \left(\left(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\leftrightarrow \left(x\cap B\subseteq B\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
10	9	rspcv	$$⊢x\cap B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\to \left(x\cap B\subseteq B\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
11	3 10	mpii	$$⊢x\cap B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
12	2 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(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
13	12	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(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
14	13	com3l	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\to \left(x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
15	14	ralrimdv	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
16		dfss	$$⊢x\subseteq B\leftrightarrow x=x\cap B$$
17	16	biimpi	$$⊢x\subseteq B\to x=x\cap B$$
18	17	oveq1d	$$⊢x\subseteq B\to x{\vee }_{\mathscr{H}}A=\left(x\cap B\right){\vee }_{\mathscr{H}}A$$
19	18	ineq1d	$$⊢x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=\left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B$$
20	17	oveq1d	$$⊢x\subseteq B\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)=\left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)$$
21	19 20	sseq12d	$$⊢x\subseteq B\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\leftrightarrow \left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
22	21	biimprcd	$$⊢\left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\to \left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
23	22	ralimi	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\to \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
24		sseq1	$$⊢x=y\to \left(x\subseteq B\leftrightarrow y\subseteq B\right)$$
25		oveq1	$$⊢x=y\to x{\vee }_{\mathscr{H}}A=y{\vee }_{\mathscr{H}}A$$
26	25	ineq1d	$$⊢x=y\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=\left(y{\vee }_{\mathscr{H}}A\right)\cap B$$
27		oveq1	$$⊢x=y\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)=y{\vee }_{\mathscr{H}}\left(A\cap B\right)$$
28	26 27	sseq12d	$$⊢x=y\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\leftrightarrow \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
29	24 28	imbi12d	$$⊢x=y\to \left(\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\leftrightarrow \left(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
30	29	cbvralvw	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\leftrightarrow \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
31	23 30	sylib	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\to \forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
32	15 31	impbid1	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}\to \left(\forall y\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
33	32	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(y\subseteq B\to \left(y{\vee }_{\mathscr{H}}A\right)\cap B\subseteq y{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(x\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
34	1 33	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\cap B\right){\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(x\cap B\right){\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$