Metamath Proof Explorer

Theorem mdslmd1i

Description: Preservation of the modular pair property in the one-to-one onto mapping between the two sublattices in Lemma 1.3 of MaedaMaeda p. 2 (meet version). (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypotheses mdslmd.1 ⊢ 𝐴 ∈ Cℋ
mdslmd.2 ⊢ 𝐵 ∈ Cℋ
mdslmd.3 ⊢ 𝐶 ∈ Cℋ
mdslmd.4 ⊢ 𝐷 ∈ Cℋ
Assertion mdslmd1i ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 𝑀ℋ 𝐷 ↔ ( 𝐶 ∩ 𝐵 ) 𝑀ℋ ( 𝐷 ∩ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 mdslmd.1 ⊢ 𝐴 ∈ Cℋ
2 mdslmd.2 ⊢ 𝐵 ∈ Cℋ
3 mdslmd.3 ⊢ 𝐶 ∈ Cℋ
4 mdslmd.4 ⊢ 𝐷 ∈ Cℋ
5 ssin ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ↔ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
6 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
7 3 4 6 chlubi ⊢ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
8 5 7 anbi12i ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ↔ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
9 chjcl ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝑥 ∨ℋ 𝐴 ) ∈ Cℋ )
10 1 9 mpan2 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∨ℋ 𝐴 ) ∈ Cℋ )
11 sseq1 ⊢ ( 𝑦 = ( 𝑥 ∨ℋ 𝐴 ) → ( 𝑦 ⊆ 𝐷 ↔ ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 ) )
12 oveq1 ⊢ ( 𝑦 = ( 𝑥 ∨ℋ 𝐴 ) → ( 𝑦 ∨ℋ 𝐶 ) = ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) )
13 12 ineq1d ⊢ ( 𝑦 = ( 𝑥 ∨ℋ 𝐴 ) → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) = ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) )
14 oveq1 ⊢ ( 𝑦 = ( 𝑥 ∨ℋ 𝐴 ) → ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) = ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
15 13 14 sseq12d ⊢ ( 𝑦 = ( 𝑥 ∨ℋ 𝐴 ) → ( ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
16 11 15 imbi12d ⊢ ( 𝑦 = ( 𝑥 ∨ℋ 𝐴 ) → ( ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ↔ ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
17 16 rspcv ⊢ ( ( 𝑥 ∨ℋ 𝐴 ) ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
18 10 17 syl ⊢ ( 𝑥 ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
19 18 adantr ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
20 1 2 3 4 mdslmd1lem3 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∨ℋ 𝐴 ) ⊆ 𝐷 → ( ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( ( 𝑥 ∨ℋ 𝐴 ) ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
21 19 20 syld ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
22 21 ex ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) ) )
23 22 com3l ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ( 𝑥 ∈ Cℋ → ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) ) )
24 23 ralrimdv ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → ∀ 𝑥 ∈ Cℋ ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
25 mdbr2 ⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ ) → ( 𝐶 𝑀ℋ 𝐷 ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
26 3 4 25 mp2an ⊢ ( 𝐶 𝑀ℋ 𝐷 ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ 𝐷 → ( ( 𝑦 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
27 3 2 chincli ⊢ ( 𝐶 ∩ 𝐵 ) ∈ Cℋ
28 4 2 chincli ⊢ ( 𝐷 ∩ 𝐵 ) ∈ Cℋ
29 27 28 mdsl2i ⊢ ( ( 𝐶 ∩ 𝐵 ) 𝑀ℋ ( 𝐷 ∩ 𝐵 ) ↔ ∀ 𝑥 ∈ Cℋ ( ( ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ 𝑥 ∧ 𝑥 ⊆ ( 𝐷 ∩ 𝐵 ) ) → ( ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑥 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) )
30 24 26 29 3imtr4g ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( 𝐶 𝑀ℋ 𝐷 → ( 𝐶 ∩ 𝐵 ) 𝑀ℋ ( 𝐷 ∩ 𝐵 ) ) )
31 chincl ⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝑥 ∩ 𝐵 ) ∈ Cℋ )
32 2 31 mpan2 ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ∩ 𝐵 ) ∈ Cℋ )
33 sseq1 ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) ↔ ( 𝑥 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) ) )
34 oveq1 ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) = ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
35 34 ineq1d ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) = ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) )
36 oveq1 ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) = ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) )
37 35 36 sseq12d ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ↔ ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) )
38 33 37 imbi12d ⊢ ( 𝑦 = ( 𝑥 ∩ 𝐵 ) → ( ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ↔ ( ( 𝑥 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
39 38 rspcv ⊢ ( ( 𝑥 ∩ 𝐵 ) ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( 𝑥 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
40 32 39 syl ⊢ ( 𝑥 ∈ Cℋ → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( 𝑥 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
41 40 adantr ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( 𝑥 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
42 1 2 3 4 mdslmd1lem4 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ( ( 𝑥 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑥 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷 ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
43 41 42 syld ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷 ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
44 43 ex ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷 ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) ) )
45 44 com3l ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( 𝑥 ∈ Cℋ → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷 ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) ) )
46 45 ralrimdv ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ∀ 𝑥 ∈ Cℋ ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷 ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
47 mdbr2 ⊢ ( ( ( 𝐶 ∩ 𝐵 ) ∈ Cℋ ∧ ( 𝐷 ∩ 𝐵 ) ∈ Cℋ ) → ( ( 𝐶 ∩ 𝐵 ) 𝑀ℋ ( 𝐷 ∩ 𝐵 ) ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) ) )
48 27 28 47 mp2an ⊢ ( ( 𝐶 ∩ 𝐵 ) 𝑀ℋ ( 𝐷 ∩ 𝐵 ) ↔ ∀ 𝑦 ∈ Cℋ ( 𝑦 ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( 𝑦 ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( 𝑦 ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) )
49 3 4 mdsl2i ⊢ ( 𝐶 𝑀ℋ 𝐷 ↔ ∀ 𝑥 ∈ Cℋ ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷 ) → ( ( 𝑥 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑥 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
50 46 48 49 3imtr4g ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( 𝐶 ∩ 𝐵 ) 𝑀ℋ ( 𝐷 ∩ 𝐵 ) → 𝐶 𝑀ℋ 𝐷 ) )
51 30 50 impbid ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( 𝐶 𝑀ℋ 𝐷 ↔ ( 𝐶 ∩ 𝐵 ) 𝑀ℋ ( 𝐷 ∩ 𝐵 ) ) )
52 8 51 sylan2br ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∨ℋ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 𝑀ℋ 𝐷 ↔ ( 𝐶 ∩ 𝐵 ) 𝑀ℋ ( 𝐷 ∩ 𝐵 ) ) )