This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrid ⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝐶 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → 𝐶 ⊆ 𝐷 ) )
29 5 28 impbid2 ⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝐶 ⊆ 𝐷 ↔ ( 𝐶 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) ) )