# Metamath Proof Explorer

## 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}}_{ℋ}$
mdslle1.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
mdslle1.3 ${⊢}{C}\in {\mathbf{C}}_{ℋ}$
mdslle1.4 ${⊢}{D}\in {\mathbf{C}}_{ℋ}$
Assertion mdslle2i ${⊢}\left({A}{𝑀}_{ℋ}{B}\wedge {A}\cap {B}\subseteq {C}\cap {D}\wedge {C}{\vee }_{ℋ}{D}\subseteq {B}\right)\to \left({C}\subseteq {D}↔{C}{\vee }_{ℋ}{A}\subseteq {D}{\vee }_{ℋ}{A}\right)$

### Proof

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