| Step | Hyp | Ref
| Expression |
| 1 | | ssin 4239 |
. . 3
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ↔ 𝐴 ⊆ (𝐶 ∩ 𝐷)) |
| 2 | | mdslmd.3 |
. . . 4
⊢ 𝐶 ∈
Cℋ |
| 3 | | mdslmd.4 |
. . . 4
⊢ 𝐷 ∈
Cℋ |
| 4 | | mdslmd.1 |
. . . . 5
⊢ 𝐴 ∈
Cℋ |
| 5 | | mdslmd.2 |
. . . . 5
⊢ 𝐵 ∈
Cℋ |
| 6 | 4, 5 | chjcli 31476 |
. . . 4
⊢ (𝐴 ∨ℋ 𝐵) ∈
Cℋ |
| 7 | 2, 3, 6 | chlubi 31490 |
. . 3
⊢ ((𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵)) |
| 8 | 1, 7 | anbi12i 628 |
. 2
⊢ (((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))) ↔ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) |
| 9 | | chjcl 31376 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (𝑥
∨ℋ 𝐴)
∈ Cℋ ) |
| 10 | 4, 9 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ 𝐴) ∈ Cℋ
) |
| 11 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 ∨ℋ 𝐴) → (𝑦 ⊆ 𝐷 ↔ (𝑥 ∨ℋ 𝐴) ⊆ 𝐷)) |
| 12 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 ∨ℋ 𝐴) → (𝑦 ∨ℋ 𝐶) = ((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶)) |
| 13 | 12 | ineq1d 4219 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 ∨ℋ 𝐴) → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) = (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷)) |
| 14 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 ∨ℋ 𝐴) → (𝑦 ∨ℋ (𝐶 ∩ 𝐷)) = ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) |
| 15 | 13, 14 | sseq12d 4017 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 ∨ℋ 𝐴) → (((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷)) ↔ (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷)))) |
| 16 | 11, 15 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑥 ∨ℋ 𝐴) → ((𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷))) ↔ ((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))))) |
| 17 | 16 | rspcv 3618 |
. . . . . . . . . 10
⊢ ((𝑥 ∨ℋ 𝐴) ∈
Cℋ → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷))) → ((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))))) |
| 18 | 10, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈
Cℋ → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷))) → ((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))))) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷))) → ((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))))) |
| 20 | 4, 5, 2, 3 | mdslmd1lem3 32346 |
. . . . . . . 8
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∨ℋ 𝐴) ⊆ 𝐷 → (((𝑥 ∨ℋ 𝐴) ∨ℋ 𝐶) ∩ 𝐷) ⊆ ((𝑥 ∨ℋ 𝐴) ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) |
| 21 | 19, 20 | syld 47 |
. . . . . . 7
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) |
| 22 | 21 | ex 412 |
. . . . . 6
⊢ (𝑥 ∈
Cℋ → (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷))) → ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))) |
| 23 | 22 | com3l 89 |
. . . . 5
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷))) → (𝑥 ∈ Cℋ
→ ((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))))) |
| 24 | 23 | ralrimdv 3152 |
. . . 4
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷))) → ∀𝑥 ∈ Cℋ
((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) |
| 25 | | mdbr2 32315 |
. . . . 5
⊢ ((𝐶 ∈
Cℋ ∧ 𝐷 ∈ Cℋ )
→ (𝐶
𝑀ℋ 𝐷 ↔ ∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷))))) |
| 26 | 2, 3, 25 | mp2an 692 |
. . . 4
⊢ (𝐶 𝑀ℋ
𝐷 ↔ ∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐷 → ((𝑦 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑦 ∨ℋ (𝐶 ∩ 𝐷)))) |
| 27 | 2, 5 | chincli 31479 |
. . . . 5
⊢ (𝐶 ∩ 𝐵) ∈
Cℋ |
| 28 | 3, 5 | chincli 31479 |
. . . . 5
⊢ (𝐷 ∩ 𝐵) ∈
Cℋ |
| 29 | 27, 28 | mdsl2i 32341 |
. . . 4
⊢ ((𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵) ↔ ∀𝑥 ∈ Cℋ
((((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ (𝐷 ∩ 𝐵)) → ((𝑥 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))) |
| 30 | 24, 26, 29 | 3imtr4g 296 |
. . 3
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (𝐶 𝑀ℋ 𝐷 → (𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵))) |
| 31 | | chincl 31518 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑥 ∩ 𝐵) ∈
Cℋ ) |
| 32 | 5, 31 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑥 ∈
Cℋ → (𝑥 ∩ 𝐵) ∈ Cℋ
) |
| 33 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 ∩ 𝐵) → (𝑦 ⊆ (𝐷 ∩ 𝐵) ↔ (𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵))) |
| 34 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 ∩ 𝐵) → (𝑦 ∨ℋ (𝐶 ∩ 𝐵)) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵))) |
| 35 | 34 | ineq1d 4219 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) = (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵))) |
| 36 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 ∩ 𝐵) → (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))) = ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) |
| 37 | 35, 36 | sseq12d 4017 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 ∩ 𝐵) → (((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))) ↔ (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))) |
| 38 | 33, 37 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑥 ∩ 𝐵) → ((𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) ↔ ((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) |
| 39 | 38 | rspcv 3618 |
. . . . . . . . . 10
⊢ ((𝑥 ∩ 𝐵) ∈ Cℋ
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → ((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) |
| 40 | 32, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈
Cℋ → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → ((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) |
| 41 | 40 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → ((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) |
| 42 | 4, 5, 2, 3 | mdslmd1lem4 32347 |
. . . . . . . 8
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (((𝑥 ∩ 𝐵) ⊆ (𝐷 ∩ 𝐵) → (((𝑥 ∩ 𝐵) ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ ((𝑥 ∩ 𝐵) ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷))))) |
| 43 | 41, 42 | syld 47 |
. . . . . . 7
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵))))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷))))) |
| 44 | 43 | ex 412 |
. . . . . 6
⊢ (𝑥 ∈
Cℋ → (((𝐴 𝑀ℋ 𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷)))))) |
| 45 | 44 | com3l 89 |
. . . . 5
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → (𝑥 ∈ Cℋ
→ (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷)))))) |
| 46 | 45 | ralrimdv 3152 |
. . . 4
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))) → ∀𝑥 ∈ Cℋ
(((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷))))) |
| 47 | | mdbr2 32315 |
. . . . 5
⊢ (((𝐶 ∩ 𝐵) ∈ Cℋ
∧ (𝐷 ∩ 𝐵) ∈
Cℋ ) → ((𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵) ↔ ∀𝑦 ∈ Cℋ
(𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵)))))) |
| 48 | 27, 28, 47 | mp2an 692 |
. . . 4
⊢ ((𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵) ↔ ∀𝑦 ∈ Cℋ
(𝑦 ⊆ (𝐷 ∩ 𝐵) → ((𝑦 ∨ℋ (𝐶 ∩ 𝐵)) ∩ (𝐷 ∩ 𝐵)) ⊆ (𝑦 ∨ℋ ((𝐶 ∩ 𝐵) ∩ (𝐷 ∩ 𝐵))))) |
| 49 | 2, 3 | mdsl2i 32341 |
. . . 4
⊢ (𝐶 𝑀ℋ
𝐷 ↔ ∀𝑥 ∈
Cℋ (((𝐶 ∩ 𝐷) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐷) → ((𝑥 ∨ℋ 𝐶) ∩ 𝐷) ⊆ (𝑥 ∨ℋ (𝐶 ∩ 𝐷)))) |
| 50 | 46, 48, 49 | 3imtr4g 296 |
. . 3
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → ((𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵) → 𝐶 𝑀ℋ 𝐷)) |
| 51 | 30, 50 | impbid 212 |
. 2
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ ((𝐴 ⊆ 𝐶 ∧ 𝐴 ⊆ 𝐷) ∧ (𝐶 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐷 ⊆ (𝐴 ∨ℋ 𝐵)))) → (𝐶 𝑀ℋ 𝐷 ↔ (𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵))) |
| 52 | 8, 51 | sylan2br 595 |
1
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝐵 𝑀ℋ*
𝐴) ∧ (𝐴 ⊆ (𝐶 ∩ 𝐷) ∧ (𝐶 ∨ℋ 𝐷) ⊆ (𝐴 ∨ℋ 𝐵))) → (𝐶 𝑀ℋ 𝐷 ↔ (𝐶 ∩ 𝐵) 𝑀ℋ (𝐷 ∩ 𝐵))) |