Theorem mdbr2

Description: Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr . (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		chub1	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to x\subseteq x{\vee }_{\mathscr{H}}A$$
3	2	ancoms	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to x\subseteq x{\vee }_{\mathscr{H}}A$$
4		iba	$$⊢x\subseteq B\to \left(x\subseteq x{\vee }_{\mathscr{H}}A\leftrightarrow \left(x\subseteq x{\vee }_{\mathscr{H}}A\wedge x\subseteq B\right)\right)$$
5		ssin	$$⊢\left(x\subseteq x{\vee }_{\mathscr{H}}A\wedge x\subseteq B\right)\leftrightarrow x\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B$$
6	4 5	bitrdi	$$⊢x\subseteq B\to \left(x\subseteq x{\vee }_{\mathscr{H}}A\leftrightarrow x\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
7	3 6	syl5ibcom	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x\subseteq B\to x\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
8		chub2	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\subseteq x{\vee }_{\mathscr{H}}A$$
9	8	ssrind	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\cap B\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B$$
10	7 9	jctird	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x\subseteq B\to \left(x\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\wedge A\cap B\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)$$
11	10	adantlr	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x\subseteq B\to \left(x\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\wedge A\cap B\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)\right)$$
12		simpr	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to x\in {\mathbf{C}}_{\mathscr{H}}$$
13		chincl	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
14	13	adantr	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
15		chjcl	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
16	15	ancoms	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
17		chincl	$$⊢\left(x{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
18	16 17	sylan	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
19	18	an32s	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
20		chlub	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge \left(x{\vee }_{\mathscr{H}}A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\wedge A\cap B\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)\leftrightarrow x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
21	12 14 19 20	syl3anc	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\wedge A\cap B\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)\leftrightarrow x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
22	11 21	sylibd	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x\subseteq B\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
23		eqss	$$⊢\left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\leftrightarrow \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\wedge x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
24	23	rbaib	$$⊢x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\leftrightarrow \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
25	22 24	syl6	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(x\subseteq B\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\leftrightarrow \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
26	25	pm5.74d	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\leftrightarrow \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)\right)$$
27	26	ralbidva	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\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)\leftrightarrow \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)\right)$$
28	1 27	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\subseteq B\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$