# 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 𝐴C
mdslle1.2 𝐵C
mdslle1.3 𝐶C
mdslle1.4 𝐷C
Assertion mdslle1i ( ( 𝐵 𝑀* 𝐴𝐴 ⊆ ( 𝐶𝐷 ) ∧ ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) ) → ( 𝐶𝐷 ↔ ( 𝐶𝐵 ) ⊆ ( 𝐷𝐵 ) ) )

### Proof

Step Hyp Ref Expression
1 mdslle1.1 𝐴C
2 mdslle1.2 𝐵C
3 mdslle1.3 𝐶C
4 mdslle1.4 𝐷C
5 ssrin ( 𝐶𝐷 → ( 𝐶𝐵 ) ⊆ ( 𝐷𝐵 ) )
6 3 2 chincli ( 𝐶𝐵 ) ∈ C
7 4 2 chincli ( 𝐷𝐵 ) ∈ C
8 6 7 1 chlej1i ( ( 𝐶𝐵 ) ⊆ ( 𝐷𝐵 ) → ( ( 𝐶𝐵 ) ∨ 𝐴 ) ⊆ ( ( 𝐷𝐵 ) ∨ 𝐴 ) )
9 id ( 𝐵 𝑀* 𝐴𝐵 𝑀* 𝐴 )
10 ssin ( ( 𝐴𝐶𝐴𝐷 ) ↔ 𝐴 ⊆ ( 𝐶𝐷 ) )
11 10 bicomi ( 𝐴 ⊆ ( 𝐶𝐷 ) ↔ ( 𝐴𝐶𝐴𝐷 ) )
12 11 simplbi ( 𝐴 ⊆ ( 𝐶𝐷 ) → 𝐴𝐶 )
13 1 2 chjcli ( 𝐴 𝐵 ) ∈ C
14 3 4 13 chlubi ( ( 𝐶 ⊆ ( 𝐴 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 𝐵 ) ) ↔ ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) )
15 14 bicomi ( ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) ↔ ( 𝐶 ⊆ ( 𝐴 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 𝐵 ) ) )
16 15 simplbi ( ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) → 𝐶 ⊆ ( 𝐴 𝐵 ) )
17 1 2 3 3pm3.2i ( 𝐴C𝐵C𝐶C )
18 dmdsl3 ( ( ( 𝐴C𝐵C𝐶C ) ∧ ( 𝐵 𝑀* 𝐴𝐴𝐶𝐶 ⊆ ( 𝐴 𝐵 ) ) ) → ( ( 𝐶𝐵 ) ∨ 𝐴 ) = 𝐶 )
19 17 18 mpan ( ( 𝐵 𝑀* 𝐴𝐴𝐶𝐶 ⊆ ( 𝐴 𝐵 ) ) → ( ( 𝐶𝐵 ) ∨ 𝐴 ) = 𝐶 )
20 9 12 16 19 syl3an ( ( 𝐵 𝑀* 𝐴𝐴 ⊆ ( 𝐶𝐷 ) ∧ ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) ) → ( ( 𝐶𝐵 ) ∨ 𝐴 ) = 𝐶 )
21 11 simprbi ( 𝐴 ⊆ ( 𝐶𝐷 ) → 𝐴𝐷 )
22 15 simprbi ( ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) → 𝐷 ⊆ ( 𝐴 𝐵 ) )
23 1 2 4 3pm3.2i ( 𝐴C𝐵C𝐷C )
24 dmdsl3 ( ( ( 𝐴C𝐵C𝐷C ) ∧ ( 𝐵 𝑀* 𝐴𝐴𝐷𝐷 ⊆ ( 𝐴 𝐵 ) ) ) → ( ( 𝐷𝐵 ) ∨ 𝐴 ) = 𝐷 )
25 23 24 mpan ( ( 𝐵 𝑀* 𝐴𝐴𝐷𝐷 ⊆ ( 𝐴 𝐵 ) ) → ( ( 𝐷𝐵 ) ∨ 𝐴 ) = 𝐷 )
26 9 21 22 25 syl3an ( ( 𝐵 𝑀* 𝐴𝐴 ⊆ ( 𝐶𝐷 ) ∧ ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) ) → ( ( 𝐷𝐵 ) ∨ 𝐴 ) = 𝐷 )
27 20 26 sseq12d ( ( 𝐵 𝑀* 𝐴𝐴 ⊆ ( 𝐶𝐷 ) ∧ ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) ) → ( ( ( 𝐶𝐵 ) ∨ 𝐴 ) ⊆ ( ( 𝐷𝐵 ) ∨ 𝐴 ) ↔ 𝐶𝐷 ) )
28 8 27 syl5ib ( ( 𝐵 𝑀* 𝐴𝐴 ⊆ ( 𝐶𝐷 ) ∧ ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) ) → ( ( 𝐶𝐵 ) ⊆ ( 𝐷𝐵 ) → 𝐶𝐷 ) )
29 5 28 impbid2 ( ( 𝐵 𝑀* 𝐴𝐴 ⊆ ( 𝐶𝐷 ) ∧ ( 𝐶 𝐷 ) ⊆ ( 𝐴 𝐵 ) ) → ( 𝐶𝐷 ↔ ( 𝐶𝐵 ) ⊆ ( 𝐷𝐵 ) ) )