Theorem mdslle2i

Description: Order preservation of the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	mdslle1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
	mdslle1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	mdslle1.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
	mdslle1.4	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	mdslle2i	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(C\subseteq D\leftrightarrow C{\vee }_{\mathscr{H}}A\subseteq D{\vee }_{\mathscr{H}}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		mdslle1.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		mdslle1.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		mdslle1.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4		mdslle1.4	$$⊢D\in {\mathbf{C}}_{\mathscr{H}}$$
5	3 4 1	chlej1i	$$⊢C\subseteq D\to C{\vee }_{\mathscr{H}}A\subseteq D{\vee }_{\mathscr{H}}A$$
6		ssrin	$$⊢C{\vee }_{\mathscr{H}}A\subseteq D{\vee }_{\mathscr{H}}A\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(D{\vee }_{\mathscr{H}}A\right)\cap B$$
7		id	$$⊢A{𝑀}_{\mathscr{H}}B\to A{𝑀}_{\mathscr{H}}B$$
8		ssin	$$⊢\left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)\leftrightarrow A\cap B\subseteq C\cap D$$
9	8	bicomi	$$⊢A\cap B\subseteq C\cap D\leftrightarrow \left(A\cap B\subseteq C\wedge A\cap B\subseteq D\right)$$
10	9	simplbi	$$⊢A\cap B\subseteq C\cap D\to A\cap B\subseteq C$$
11	3 4 2	chlubi	$$⊢\left(C\subseteq B\wedge D\subseteq B\right)\leftrightarrow C{\vee }_{\mathscr{H}}D\subseteq B$$
12	11	bicomi	$$⊢C{\vee }_{\mathscr{H}}D\subseteq B\leftrightarrow \left(C\subseteq B\wedge D\subseteq B\right)$$
13	12	simplbi	$$⊢C{\vee }_{\mathscr{H}}D\subseteq B\to C\subseteq B$$
14	1 2 3	3pm3.2i	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)$$
15		mdsl3	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge C\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\wedge C\subseteq B\right)\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C$$
16	14 15	mpan	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\wedge C\subseteq B\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C$$
17	7 10 13 16	syl3an	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(C{\vee }_{\mathscr{H}}A\right)\cap B=C$$
18	9	simprbi	$$⊢A\cap B\subseteq C\cap D\to A\cap B\subseteq D$$
19	12	simprbi	$$⊢C{\vee }_{\mathscr{H}}D\subseteq B\to D\subseteq B$$
20	1 2 4	3pm3.2i	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)$$
21		mdsl3	$$⊢\left(\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge D\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq D\wedge D\subseteq B\right)\right)\to \left(D{\vee }_{\mathscr{H}}A\right)\cap B=D$$
22	20 21	mpan	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq D\wedge D\subseteq B\right)\to \left(D{\vee }_{\mathscr{H}}A\right)\cap B=D$$
23	7 18 19 22	syl3an	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(D{\vee }_{\mathscr{H}}A\right)\cap B=D$$
24	17 23	sseq12d	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(\left(C{\vee }_{\mathscr{H}}A\right)\cap B\subseteq \left(D{\vee }_{\mathscr{H}}A\right)\cap B\leftrightarrow C\subseteq D\right)$$
25	6 24	imbitrid	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(C{\vee }_{\mathscr{H}}A\subseteq D{\vee }_{\mathscr{H}}A\to C\subseteq D\right)$$
26	5 25	impbid2	$$⊢\left(A{𝑀}_{\mathscr{H}}B\wedge A\cap B\subseteq C\cap D\wedge C{\vee }_{\mathscr{H}}D\subseteq B\right)\to \left(C\subseteq D\leftrightarrow C{\vee }_{\mathscr{H}}A\subseteq D{\vee }_{\mathscr{H}}A\right)$$