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

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 ⊢ 𝐴 ∈ Cℋ
mdslle1.2 ⊢ 𝐵 ∈ Cℋ
mdslle1.3 ⊢ 𝐶 ∈ Cℋ
mdslle1.4 ⊢ 𝐷 ∈ Cℋ
Assertion mdslle2i ( ( 𝐴 𝑀ℋ 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ 𝐵 ) → ( 𝐶 ⊆ 𝐷 ↔ ( 𝐶 ∨ℋ 𝐴 ) ⊆ ( 𝐷 ∨ℋ 𝐴 ) ) )

Proof

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