# Metamath Proof Explorer

## Theorem mdslle1i

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