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

Metamath Proof Explorer

Theorem mdslmd1lem2

Description: Lemma for mdslmd1i . (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 mdslmd.1 ⊢ 𝐴 ∈ Cℋ
2 mdslmd.2 ⊢ 𝐵 ∈ Cℋ
3 mdslmd.3 ⊢ 𝐶 ∈ Cℋ
4 mdslmd.4 ⊢ 𝐷 ∈ Cℋ
5 mdslmd1lem.5 ⊢ 𝑅 ∈ Cℋ
6 ssrin ⊢ ( 𝑅 ⊆ 𝐷 → ( 𝑅 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) )
7 6 adantl ⊢ ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( 𝑅 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) )
8 7 imim1i ⊢ ( ( ( 𝑅 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) )
9 simpllr ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐵 𝑀ℋ* 𝐴 )
10 3 5 chub2i ⊢ 𝐶 ⊆ ( 𝑅 ∨ℋ 𝐶 )
11 sstr ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ ( 𝑅 ∨ℋ 𝐶 ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐶 ) )
12 10 11 mpan2 ⊢ ( 𝐴 ⊆ 𝐶 → 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐶 ) )
13 12 ad2antrr ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐶 ) )
14 13 ad2antlr ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ 𝐶 ) )
15 simplr ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐴 ⊆ 𝐷 )
16 15 ad2antlr ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ 𝐷 )
17 14 16 ssind ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) )
18 ssin ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ↔ 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
19 3 4 chincli ⊢ ( 𝐶 ∩ 𝐷 ) ∈ Cℋ
20 19 5 chub2i ⊢ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) )
21 sstr ⊢ ( ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
22 20 21 mpan2 ⊢ ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
23 18 22 sylbi ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
24 23 adantr ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
25 24 ad2antlr ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) )
26 17 25 ssind ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) )
27 inss2 ⊢ ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ 𝐷
28 sstr ⊢ ( ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
29 27 28 mpan ⊢ ( 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
30 29 ad2antll ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
31 30 ad2antlr ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
32 sstr ⊢ ( ( 𝑅 ⊆ 𝐷 ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
33 32 ancoms ⊢ ( ( 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝑅 ⊆ 𝐷 ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
34 33 ad2ant2l ⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
35 34 adantll ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
36 35 adantll ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
37 ssinss1 ⊢ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
38 37 ad2antrl ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
39 38 ad2antlr ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
40 36 39 jca ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
41 1 2 chjcli ⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ
42 5 19 41 chlubi ⊢ ( ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
43 40 42 sylib ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
44 31 43 jca ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
45 5 3 chjcli ⊢ ( 𝑅 ∨ℋ 𝐶 ) ∈ Cℋ
46 45 4 chincli ⊢ ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∈ Cℋ
47 5 19 chjcli ⊢ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∈ Cℋ
48 46 47 41 chlubi ⊢ ( ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∨ℋ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
49 44 48 sylib ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∨ℋ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
50 1 2 46 47 mdslle1i ⊢ ( ( 𝐵 𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ∧ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∨ℋ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) ) )
51 9 26 49 50 syl3anc ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) ) )
52 inindir ⊢ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) = ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) )
53 sstr ⊢ ( ( 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) → 𝐴 ⊆ 𝑅 )
54 18 53 sylanb ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) → 𝐴 ⊆ 𝑅 )
55 54 ad2ant2r ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ 𝑅 )
56 simplll ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ 𝐶 )
57 55 56 ssind ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐴 ⊆ ( 𝑅 ∩ 𝐶 ) )
58 simplrl ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
59 35 58 jca ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
60 5 3 41 chlubi ⊢ ( ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ↔ ( 𝑅 ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
61 59 60 sylib ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝑅 ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
62 57 61 jca ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝐴 ⊆ ( 𝑅 ∩ 𝐶 ) ∧ ( 𝑅 ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
63 1 2 5 3 mdslj1i ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝑅 ∩ 𝐶 ) ∧ ( 𝑅 ∨ℋ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
64 62 63 sylan2 ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
65 64 anassrs ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) )
66 65 ineq1d ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) = ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) )
67 52 66 eqtr2id ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) = ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) )
68 18 biimpi ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) → 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
69 68 adantr ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) → 𝐴 ⊆ ( 𝐶 ∩ 𝐷 ) )
70 54 69 ssind ⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) → 𝐴 ⊆ ( 𝑅 ∩ ( 𝐶 ∩ 𝐷 ) ) )
71 33 adantll ⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) → 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
72 37 ad2antrr ⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
73 71 72 jca ⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) → ( 𝑅 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
74 73 42 sylib ⊢ ( ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) → ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) )
75 70 74 anim12i ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ) ∧ ( ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝐴 ⊆ ( 𝑅 ∩ ( 𝐶 ∩ 𝐷 ) ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
76 75 an4s ⊢ ( ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( 𝐴 ⊆ ( 𝑅 ∩ ( 𝐶 ∩ 𝐷 ) ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) )
77 1 2 5 19 mdslj1i ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( 𝐴 ⊆ ( 𝑅 ∩ ( 𝐶 ∩ 𝐷 ) ) ∧ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) )
78 76 77 sylan2 ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) )
79 78 anassrs ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) )
80 inindir ⊢ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) )
81 80 a1i ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) = ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) )
82 81 oveq2d ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐷 ) ∩ 𝐵 ) ) = ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) )
83 79 82 eqtr2d ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) = ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) )
84 67 83 sseq12d ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ↔ ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ∩ 𝐵 ) ⊆ ( ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ∩ 𝐵 ) ) )
85 51 84 bitr4d ⊢ ( ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) ∧ ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) ) → ( ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ↔ ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) )
86 85 exbiri ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
87 86 a2d ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )
88 8 87 syl5 ⊢ ( ( ( 𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ* 𝐴 ) ∧ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷 ) ∧ ( 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝐷 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) → ( ( ( 𝑅 ∩ 𝐵 ) ⊆ ( 𝐷 ∩ 𝐵 ) → ( ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( 𝐶 ∩ 𝐵 ) ) ∩ ( 𝐷 ∩ 𝐵 ) ) ⊆ ( ( 𝑅 ∩ 𝐵 ) ∨ℋ ( ( 𝐶 ∩ 𝐵 ) ∩ ( 𝐷 ∩ 𝐵 ) ) ) ) → ( ( ( 𝐶 ∩ 𝐷 ) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷 ) → ( ( 𝑅 ∨ℋ 𝐶 ) ∩ 𝐷 ) ⊆ ( 𝑅 ∨ℋ ( 𝐶 ∩ 𝐷 ) ) ) ) )