Theorem mdsl2bi

Description: If the modular pair property holds in a sublattice, it holds in the whole lattice. Lemma 1.4 of MaedaMaeda p. 2. (Contributed by NM, 24-Dec-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdsl.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mdsl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	mdsl2bi	$$⊢A{𝑀}_{\mathscr{H}}B\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdsl.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdsl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	mdsl2i	$$⊢A{𝑀}_{\mathscr{H}}B\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
4	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
5		inss1	$$⊢A\cap B\subseteq A$$
6		chlej2	$$⊢\left(\left(A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge A\cap B\subseteq A\right)\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq x{\vee }_{\mathscr{H}}A$$
7	5 6	mpan2	$$⊢\left(A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq x{\vee }_{\mathscr{H}}A$$
8	4 1 7	mp3an12	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq x{\vee }_{\mathscr{H}}A$$
9	8	adantr	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq x{\vee }_{\mathscr{H}}A$$
10		simpr	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\to x\subseteq B$$
11		inss2	$$⊢A\cap B\subseteq B$$
12	10 11	jctir	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\to \left(x\subseteq B\wedge A\cap B\subseteq B\right)$$
13		chlub	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge A\cap B\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(\left(x\subseteq B\wedge A\cap B\subseteq B\right)\leftrightarrow x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq B\right)$$
14	4 2 13	mp3an23	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(x\subseteq B\wedge A\cap B\subseteq B\right)\leftrightarrow x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq B\right)$$
15	14	adantr	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\to \left(\left(x\subseteq B\wedge A\cap B\subseteq B\right)\leftrightarrow x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq B\right)$$
16	12 15	mpbid	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq B$$
17	9 16	ssind	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\to x{\vee }_{\mathscr{H}}\left(A\cap B\right)\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B$$
18	17	biantrud	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\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{\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)\right)$$
19		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)$$
20	18 19	bitr4di	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge x\subseteq B\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\leftrightarrow \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
21	20	ex	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(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(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
22	21	adantld	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(\left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\leftrightarrow \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
23	22	pm5.74d	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(\left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\leftrightarrow \left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
24	23	ralbiia	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$
25	3 24	bitri	$$⊢A{𝑀}_{\mathscr{H}}B\leftrightarrow \forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(A\cap B\subseteq x\wedge x\subseteq B\right)\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B=x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)$$