Theorem mdsl2i

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, 28-Apr-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	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)$$

Proof

Step	Hyp	Ref	Expression
1		mdsl.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdsl.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		chub1	$$⊢\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to x\subseteq x{\vee }_{\mathscr{H}}A$$
4	1 3	mpan2	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to x\subseteq x{\vee }_{\mathscr{H}}A$$
5		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)$$
6		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$$
7	5 6	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)$$
8	4 7	syl5ibcom	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x\subseteq B\to x\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B\right)$$
9		chub2	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\subseteq x{\vee }_{\mathscr{H}}A$$
10	1 9	mpan	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to A\subseteq x{\vee }_{\mathscr{H}}A$$
11	10	ssrind	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to A\cap B\subseteq \left(x{\vee }_{\mathscr{H}}A\right)\cap B$$
12	8 11	jctird	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\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)$$
13		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}}$$
14	1 13	mpan2	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to x{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}$$
15		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}}$$
16	2 15	mpan2	$$⊢x{\vee }_{\mathscr{H}}A\in {\mathbf{C}}_{\mathscr{H}}\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
17	14 16	syl	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\to \left(x{\vee }_{\mathscr{H}}A\right)\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
18	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
19		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)$$
20	18 19	mp3an2	$$⊢\left(x\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	17 20	mpdan	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\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	12 21	sylibd	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\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	$$⊢x\in {\mathbf{C}}_{\mathscr{H}}\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	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=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)$$
27	26	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=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\subseteq x{\vee }_{\mathscr{H}}\left(A\cap B\right)\right)\right)$$
28	2 1	chub2i	$$⊢B\subseteq A{\vee }_{\mathscr{H}}B$$
29		sstr	$$⊢\left(x\subseteq B\wedge B\subseteq A{\vee }_{\mathscr{H}}B\right)\to x\subseteq A{\vee }_{\mathscr{H}}B$$
30	28 29	mpan2	$$⊢x\subseteq B\to x\subseteq A{\vee }_{\mathscr{H}}B$$
31	30	pm4.71ri	$$⊢x\subseteq B\leftrightarrow \left(x\subseteq A{\vee }_{\mathscr{H}}B\wedge x\subseteq B\right)$$
32	31	anbi2i	$$⊢\left(A\cap B\subseteq x\wedge x\subseteq B\right)\leftrightarrow \left(A\cap B\subseteq x\wedge \left(x\subseteq A{\vee }_{\mathscr{H}}B\wedge x\subseteq B\right)\right)$$
33		anass	$$⊢\left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\wedge x\subseteq B\right)\leftrightarrow \left(A\cap B\subseteq x\wedge \left(x\subseteq A{\vee }_{\mathscr{H}}B\wedge x\subseteq B\right)\right)$$
34	32 33	bitr4i	$$⊢\left(A\cap B\subseteq x\wedge x\subseteq B\right)\leftrightarrow \left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\wedge x\subseteq B\right)$$
35	34	imbi1i	$$⊢\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)\leftrightarrow \left(\left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\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)$$
36	27 35	bitr3di	$$⊢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(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\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)$$
37		impexp	$$⊢\left(\left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\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)\leftrightarrow \left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \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)$$
38	36 37	bitrdi	$$⊢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 A{\vee }_{\mathscr{H}}B\right)\to \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)\right)$$
39	38	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 A{\vee }_{\mathscr{H}}B\right)\to \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)$$
40	1 2	mdsl1i	$$⊢\forall x\in {\mathbf{C}}_{\mathscr{H}}\left(\left(A\cap B\subseteq x\wedge x\subseteq A{\vee }_{\mathscr{H}}B\right)\to \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)\leftrightarrow A{𝑀}_{\mathscr{H}}B$$
41	39 40	bitr2i	$$⊢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)$$