Proof of Theorem mdslmd1lem2
Step | Hyp | Ref
| Expression |
1 | | ssrin 4138 |
. . . 4
⊢ (𝑅 ⊆ 𝐷 → (𝑅 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵)) |
2 | 1 | adantl 485 |
. . 3
⊢ (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → (𝑅 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵)) |
3 | 2 | imim1i 63 |
. 2
⊢ (((𝑅 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))) |
4 | | simpllr 776 |
. . . . . 6
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐵 𝑀ℋ*
𝐴) |
5 | | mdslmd.3 |
. . . . . . . . . . . 12
⊢ 𝐶 ∈
Cℋ |
6 | | mdslmd1lem.5 |
. . . . . . . . . . . 12
⊢ 𝑅 ∈
Cℋ |
7 | 5, 6 | chub2i 29523 |
. . . . . . . . . . 11
⊢ 𝐶 ⊆ (𝑅 ∨ℋ 𝐶) |
8 | | sstr 3899 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊆ (𝑅 ∨ℋ 𝐶)) → 𝐴 ⊆ (𝑅 ∨ℋ 𝐶)) |
9 | 7, 8 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝐶 → 𝐴 ⊆ (𝑅 ∨ℋ 𝐶)) |
10 | 9 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝐴 ⊆ (𝑅 ∨ℋ 𝐶)) |
11 | 10 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐴 ⊆ (𝑅 ∨ℋ 𝐶)) |
12 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝐴 ⊆ 𝐷) |
13 | 12 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐴 ⊆ 𝐷) |
14 | 11, 13 | ssind 4137 |
. . . . . . 7
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐴 ⊆ ((𝑅 ∨ℋ 𝐶) ∩ 𝐷)) |
15 | | ssin 4135 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ↔ 𝐴 ⊆ (𝐶 ∩ 𝐷)) |
16 | | mdslmd.4 |
. . . . . . . . . . . . 13
⊢ 𝐷 ∈
Cℋ |
17 | 5, 16 | chincli 29513 |
. . . . . . . . . . . 12
⊢ (𝐶 ∩ 𝐷) ∈
Cℋ |
18 | 17, 6 | chub2i 29523 |
. . . . . . . . . . 11
⊢ (𝐶 ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) |
19 | | sstr 3899 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) → 𝐴 ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) |
20 | 18, 19 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ (𝐶 ∩ 𝐷) → 𝐴 ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) |
21 | 15, 20 | sylbi 220 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) → 𝐴 ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) |
22 | 21 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → 𝐴 ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) |
23 | 22 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐴 ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) |
24 | 14, 23 | ssind 4137 |
. . . . . 6
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐴 ⊆ (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∩ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)))) |
25 | | inss2 4134 |
. . . . . . . . . . 11
⊢ ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ 𝐷 |
26 | | sstr 3899 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
27 | 25, 26 | mpan 690 |
. . . . . . . . . 10
⊢ (𝐷 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
28 | 27 | ad2antll 729 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
29 | 28 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
30 | | sstr 3899 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ⊆ 𝐷 ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵)) |
31 | 30 | ancoms 462 |
. . . . . . . . . . . . 13
⊢ ((𝐷 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝑅 ⊆ 𝐷) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵)) |
32 | 31 | ad2ant2l 746 |
. . . . . . . . . . . 12
⊢ (((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵)) |
33 | 32 | adantll 714 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵)) |
34 | 33 | adantll 714 |
. . . . . . . . . 10
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵)) |
35 | | ssinss1 4142 |
. . . . . . . . . . . 12
⊢ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) → (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
36 | 35 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
37 | 36 | ad2antlr 727 |
. . . . . . . . . 10
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
38 | 34, 37 | jca 515 |
. . . . . . . . 9
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (𝑅 ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) |
39 | | mdslmd.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈
Cℋ |
40 | | mdslmd.2 |
. . . . . . . . . . 11
⊢ 𝐵 ∈
Cℋ |
41 | 39, 40 | chjcli 29510 |
. . . . . . . . . 10
⊢ (𝐴 ∨ℋ 𝐵) ∈
Cℋ |
42 | 6, 17, 41 | chlubi 29524 |
. . . . . . . . 9
⊢ ((𝑅 ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵)) |
43 | 38, 42 | sylib 221 |
. . . . . . . 8
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵)) |
44 | 29, 43 | jca 515 |
. . . . . . 7
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵))) |
45 | 6, 5 | chjcli 29510 |
. . . . . . . . 9
⊢ (𝑅 ∨ℋ 𝐶) ∈
Cℋ |
46 | 45, 16 | chincli 29513 |
. . . . . . . 8
⊢ ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∈
Cℋ |
47 | 6, 17 | chjcli 29510 |
. . . . . . . 8
⊢ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ∈
Cℋ |
48 | 46, 47, 41 | chlubi 29524 |
. . . . . . 7
⊢ ((((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∨ℋ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) ⊆ (𝐴 ∨ℋ 𝐵)) |
49 | 44, 48 | sylib 221 |
. . . . . 6
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∨ℋ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) ⊆ (𝐴 ∨ℋ 𝐵)) |
50 | 39, 40, 46, 47 | mdslle1i 30370 |
. . . . . 6
⊢ ((𝐵
𝑀ℋ* 𝐴 ∧ 𝐴 ⊆ (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∩ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) ∧ (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∨ℋ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))) ⊆ (𝐴 ∨ℋ 𝐵)) → (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ↔ (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵) ⊆ ((𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵))) |
51 | 4, 24, 49, 50 | syl3anc 1373 |
. . . . 5
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ↔ (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵) ⊆ ((𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵))) |
52 | | inindir 4132 |
. . . . . . 7
⊢ (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵) = (((𝑅 ∨ℋ 𝐶) ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) |
53 | | sstr 3899 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∩ 𝐷) ⊆ 𝑅) → 𝐴 ⊆ 𝑅) |
54 | 15, 53 | sylanb 584 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ∩ 𝐷) ⊆ 𝑅) → 𝐴 ⊆ 𝑅) |
55 | 54 | ad2ant2r 747 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐴 ⊆ 𝑅) |
56 | | simplll 775 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐴 ⊆ 𝐶) |
57 | 55, 56 | ssind 4137 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐴 ⊆ (𝑅 ∩ 𝐶)) |
58 | | simplrl 777 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → 𝐶 ⊆ (𝐴 ∨ℋ 𝐵)) |
59 | 33, 58 | jca 515 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (𝑅 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵))) |
60 | 6, 5, 41 | chlubi 29524 |
. . . . . . . . . . . 12
⊢ ((𝑅 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐶 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝑅 ∨ℋ 𝐶) ⊆ (𝐴 ∨ℋ 𝐵)) |
61 | 59, 60 | sylib 221 |
. . . . . . . . . . 11
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (𝑅 ∨ℋ 𝐶) ⊆ (𝐴 ∨ℋ 𝐵)) |
62 | 57, 61 | jca 515 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (𝐴 ⊆ (𝑅 ∩ 𝐶) ∧ (𝑅 ∨ℋ 𝐶) ⊆ (𝐴 ∨ℋ 𝐵))) |
63 | 39, 40, 6, 5 | mdslj1i 30372 |
. . . . . . . . . 10
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ (𝑅 ∩ 𝐶) ∧ (𝑅 ∨ℋ 𝐶) ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐵) = ((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵))) |
64 | 62, 63 | sylan2 596 |
. . . . . . . . 9
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷))) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐵) = ((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵))) |
65 | 64 | anassrs 471 |
. . . . . . . 8
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐵) = ((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵))) |
66 | 65 | ineq1d 4116 |
. . . . . . 7
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (((𝑅 ∨ℋ 𝐶) ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) = (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵))) |
67 | 52, 66 | eqtr2id 2787 |
. . . . . 6
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) = (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵)) |
68 | 15 | biimpi 219 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) → 𝐴 ⊆ (𝐶 ∩ 𝐷)) |
69 | 68 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ∩ 𝐷) ⊆ 𝑅) → 𝐴 ⊆ (𝐶 ∩ 𝐷)) |
70 | 54, 69 | ssind 4137 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ∩ 𝐷) ⊆ 𝑅) → 𝐴 ⊆ (𝑅 ∩ (𝐶 ∩ 𝐷))) |
71 | 31 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝑅 ⊆ 𝐷) → 𝑅 ⊆ (𝐴 ∨ℋ 𝐵)) |
72 | 35 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝑅 ⊆ 𝐷) → (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
73 | 71, 72 | jca 515 |
. . . . . . . . . . . 12
⊢ (((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝑅 ⊆ 𝐷) → (𝑅 ⊆ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) |
74 | 73, 42 | sylib 221 |
. . . . . . . . . . 11
⊢ (((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝑅 ⊆ 𝐷) → (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵)) |
75 | 70, 74 | anim12i 616 |
. . . . . . . . . 10
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ∩ 𝐷) ⊆ 𝑅) ∧ ((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) ∧ 𝑅 ⊆ 𝐷)) → (𝐴 ⊆ (𝑅 ∩ (𝐶 ∩ 𝐷)) ∧ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵))) |
76 | 75 | an4s 660 |
. . . . . . . . 9
⊢ ((((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (𝐴 ⊆ (𝑅 ∩ (𝐶 ∩ 𝐷)) ∧ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵))) |
77 | 39, 40, 6, 17 | mdslj1i 30372 |
. . . . . . . . 9
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ (𝑅 ∩ (𝐶 ∩ 𝐷)) ∧ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵) = ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐷) ∩ 𝐵))) |
78 | 76, 77 | sylan2 596 |
. . . . . . . 8
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷))) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵) = ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐷) ∩ 𝐵))) |
79 | 78 | anassrs 471 |
. . . . . . 7
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → ((𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵) = ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐷) ∩ 𝐵))) |
80 | | inindir 4132 |
. . . . . . . . 9
⊢ ((𝐶 ∩ 𝐷) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) |
81 | 80 | a1i 11 |
. . . . . . . 8
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → ((𝐶 ∩ 𝐷) ∩ 𝐵) = ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))) |
82 | 81 | oveq2d 7218 |
. . . . . . 7
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐷) ∩ 𝐵)) = ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) |
83 | 79, 82 | eqtr2d 2775 |
. . . . . 6
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))) = ((𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵)) |
84 | 67, 83 | sseq12d 3924 |
. . . . 5
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → ((((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))) ↔ (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ∩ 𝐵) ⊆ ((𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ∩ 𝐵))) |
85 | 51, 84 | bitr4d 285 |
. . . 4
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) ∧ ((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷)) → (((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷)) ↔ (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))) |
86 | 85 | exbiri 811 |
. . 3
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → ((((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))))) |
87 | 86 | a2d 29 |
. 2
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → ((((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))))) |
88 | 3, 87 | syl5 34 |
1
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (((𝑅 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑅 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑅 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑅 ∧ 𝑅 ⊆ 𝐷) → ((𝑅 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑅 ∨ℋ (𝐶 ∩ 𝐷))))) |