Step | Hyp | Ref
| Expression |
1 | | mdslmd.4 |
. . . . . . . . . . 11
⊢ 𝐷 ∈
Cℋ |
2 | | mdslmd.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈
Cℋ |
3 | | chlej2 27754 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) ∧ 𝐷 ⊆ 𝐴) → (𝑥 ∨ℋ 𝐷) ⊆ (𝑥 ∨ℋ 𝐴)) |
4 | 3 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → (𝐷 ⊆ 𝐴 → (𝑥 ∨ℋ 𝐷) ⊆ (𝑥 ∨ℋ 𝐴))) |
5 | 1, 2, 4 | mp3an12 1406 |
. . . . . . . . . 10
⊢ (𝑥 ∈
Cℋ → (𝐷 ⊆ 𝐴 → (𝑥 ∨ℋ 𝐷) ⊆ (𝑥 ∨ℋ 𝐴))) |
6 | 5 | impcom 445 |
. . . . . . . . 9
⊢ ((𝐷 ⊆ 𝐴 ∧ 𝑥 ∈ Cℋ )
→ (𝑥
∨ℋ 𝐷)
⊆ (𝑥
∨ℋ 𝐴)) |
7 | | ssrin 3800 |
. . . . . . . . 9
⊢ ((𝑥 ∨ℋ 𝐷) ⊆ (𝑥 ∨ℋ 𝐴) → ((𝑥 ∨ℋ 𝐷) ∩ (𝐵 ∩ 𝐶)) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶))) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
⊢ ((𝐷 ⊆ 𝐴 ∧ 𝑥 ∈ Cℋ )
→ ((𝑥
∨ℋ 𝐷)
∩ (𝐵 ∩ 𝐶)) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶))) |
9 | 8 | adantll 746 |
. . . . . . 7
⊢ ((((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴) ∧ 𝑥 ∈ Cℋ )
→ ((𝑥
∨ℋ 𝐷)
∩ (𝐵 ∩ 𝐶)) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶))) |
10 | 9 | adantll 746 |
. . . . . 6
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) ∧ 𝑥 ∈ Cℋ )
→ ((𝑥
∨ℋ 𝐷)
∩ (𝐵 ∩ 𝐶)) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶))) |
11 | 10 | adantr 480 |
. . . . 5
⊢
(((((𝐴
𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) ∧ 𝑥 ∈ Cℋ )
∧ 𝑥 ⊆ (𝐵 ∩ 𝐶)) → ((𝑥 ∨ℋ 𝐷) ∩ (𝐵 ∩ 𝐶)) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶))) |
12 | | ssin 3797 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶) ↔ 𝑥 ⊆ (𝐵 ∩ 𝐶)) |
13 | | inass 3785 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ∩ 𝐶) = ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶)) |
14 | | mdslmd.2 |
. . . . . . . . . . . . . . . 16
⊢ 𝐵 ∈
Cℋ |
15 | | mdi 28538 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵)) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) |
16 | 2, 15 | mp3anl1 1410 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
∧ (𝐴
𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵)) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) |
17 | 14, 16 | mpanl1 712 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵)) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) |
18 | 17 | ineq1d 3775 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵)) → (((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ∩ 𝐶) = ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶)) |
19 | 13, 18 | syl5eqr 2658 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵)) → ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶)) = ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶)) |
20 | 19 | adantrlr 755 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ 𝑥 ⊆ 𝐵)) → ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶)) = ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶)) |
21 | 20 | adantrrr 757 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ (𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶))) → ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶)) = ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶)) |
22 | | mdslmd.3 |
. . . . . . . . . . . . . . 15
⊢ 𝐶 ∈
Cℋ |
23 | 2, 14 | chincli 27703 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∩ 𝐵) ∈
Cℋ |
24 | | mdi 28538 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∩ 𝐵) ∈ Cℋ
∧ 𝐶 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) 𝑀ℋ
𝐶 ∧ 𝑥 ⊆ 𝐶)) → ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶) = (𝑥 ∨ℋ ((𝐴 ∩ 𝐵) ∩ 𝐶))) |
25 | 23, 24 | mp3anl1 1410 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) 𝑀ℋ
𝐶 ∧ 𝑥 ⊆ 𝐶)) → ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶) = (𝑥 ∨ℋ ((𝐴 ∩ 𝐵) ∩ 𝐶))) |
26 | 22, 25 | mpanl1 712 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 ∩ 𝐵) 𝑀ℋ 𝐶 ∧ 𝑥 ⊆ 𝐶)) → ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶) = (𝑥 ∨ℋ ((𝐴 ∩ 𝐵) ∩ 𝐶))) |
27 | | inass 3785 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∩ 𝐵) ∩ 𝐶) = (𝐴 ∩ (𝐵 ∩ 𝐶)) |
28 | 27 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∨ℋ ((𝐴 ∩ 𝐵) ∩ 𝐶)) = (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶))) |
29 | 26, 28 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 ∩ 𝐵) 𝑀ℋ 𝐶 ∧ 𝑥 ⊆ 𝐶)) → ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶) = (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
30 | 29 | adantrll 754 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ 𝑥 ⊆ 𝐶)) → ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶) = (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
31 | 30 | adantrrl 756 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ (𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶))) → ((𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ∩ 𝐶) = (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
32 | 21, 31 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
Cℋ ∧ ((𝐴 𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ (𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶))) → ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶)) = (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
33 | 32 | ancoms 468 |
. . . . . . . . 9
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ (𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶)) ∧ 𝑥 ∈ Cℋ )
→ ((𝑥
∨ℋ 𝐴)
∩ (𝐵 ∩ 𝐶)) = (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
34 | 33 | an32s 842 |
. . . . . . . 8
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ 𝑥 ∈ Cℋ )
∧ (𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐶)) → ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶)) = (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
35 | 12, 34 | sylan2br 492 |
. . . . . . 7
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ 𝑥 ∈ Cℋ )
∧ 𝑥 ⊆ (𝐵 ∩ 𝐶)) → ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶)) = (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
36 | 35 | adantllr 751 |
. . . . . 6
⊢
(((((𝐴
𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) ∧ 𝑥 ∈ Cℋ )
∧ 𝑥 ⊆ (𝐵 ∩ 𝐶)) → ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶)) = (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
37 | | inass 3785 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) = (𝐴 ∩ (𝐶 ∩ (𝐵 ∩ 𝐶))) |
38 | | in12 3786 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ (𝐶 ∩ 𝐶)) |
39 | | inidm 3784 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∩ 𝐶) = 𝐶 |
40 | 39 | ineq2i 3773 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∩ (𝐶 ∩ 𝐶)) = (𝐵 ∩ 𝐶) |
41 | 38, 40 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∩ (𝐵 ∩ 𝐶)) = (𝐵 ∩ 𝐶) |
42 | 41 | ineq2i 3773 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ (𝐶 ∩ (𝐵 ∩ 𝐶))) = (𝐴 ∩ (𝐵 ∩ 𝐶)) |
43 | 37, 42 | eqtr2i 2633 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ (𝐵 ∩ 𝐶)) = ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) |
44 | | ssrin 3800 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐶) ⊆ 𝐷 → ((𝐴 ∩ 𝐶) ∩ (𝐵 ∩ 𝐶)) ⊆ (𝐷 ∩ (𝐵 ∩ 𝐶))) |
45 | 43, 44 | syl5eqss 3612 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ 𝐶) ⊆ 𝐷 → (𝐴 ∩ (𝐵 ∩ 𝐶)) ⊆ (𝐷 ∩ (𝐵 ∩ 𝐶))) |
46 | | ssrin 3800 |
. . . . . . . . . 10
⊢ (𝐷 ⊆ 𝐴 → (𝐷 ∩ (𝐵 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∩ 𝐶))) |
47 | 45, 46 | anim12i 588 |
. . . . . . . . 9
⊢ (((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴) → ((𝐴 ∩ (𝐵 ∩ 𝐶)) ⊆ (𝐷 ∩ (𝐵 ∩ 𝐶)) ∧ (𝐷 ∩ (𝐵 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
48 | | eqss 3583 |
. . . . . . . . 9
⊢ ((𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐷 ∩ (𝐵 ∩ 𝐶)) ↔ ((𝐴 ∩ (𝐵 ∩ 𝐶)) ⊆ (𝐷 ∩ (𝐵 ∩ 𝐶)) ∧ (𝐷 ∩ (𝐵 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∩ 𝐶)))) |
49 | 47, 48 | sylibr 223 |
. . . . . . . 8
⊢ (((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴) → (𝐴 ∩ (𝐵 ∩ 𝐶)) = (𝐷 ∩ (𝐵 ∩ 𝐶))) |
50 | 49 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴) → (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶))) = (𝑥 ∨ℋ (𝐷 ∩ (𝐵 ∩ 𝐶)))) |
51 | 50 | ad3antlr 763 |
. . . . . 6
⊢
(((((𝐴
𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) ∧ 𝑥 ∈ Cℋ )
∧ 𝑥 ⊆ (𝐵 ∩ 𝐶)) → (𝑥 ∨ℋ (𝐴 ∩ (𝐵 ∩ 𝐶))) = (𝑥 ∨ℋ (𝐷 ∩ (𝐵 ∩ 𝐶)))) |
52 | 36, 51 | eqtrd 2644 |
. . . . 5
⊢
(((((𝐴
𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) ∧ 𝑥 ∈ Cℋ )
∧ 𝑥 ⊆ (𝐵 ∩ 𝐶)) → ((𝑥 ∨ℋ 𝐴) ∩ (𝐵 ∩ 𝐶)) = (𝑥 ∨ℋ (𝐷 ∩ (𝐵 ∩ 𝐶)))) |
53 | 11, 52 | sseqtrd 3604 |
. . . 4
⊢
(((((𝐴
𝑀ℋ 𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) ∧ 𝑥 ∈ Cℋ )
∧ 𝑥 ⊆ (𝐵 ∩ 𝐶)) → ((𝑥 ∨ℋ 𝐷) ∩ (𝐵 ∩ 𝐶)) ⊆ (𝑥 ∨ℋ (𝐷 ∩ (𝐵 ∩ 𝐶)))) |
54 | 53 | ex 449 |
. . 3
⊢ ((((𝐴 𝑀ℋ
𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) ∧ 𝑥 ∈ Cℋ )
→ (𝑥 ⊆ (𝐵 ∩ 𝐶) → ((𝑥 ∨ℋ 𝐷) ∩ (𝐵 ∩ 𝐶)) ⊆ (𝑥 ∨ℋ (𝐷 ∩ (𝐵 ∩ 𝐶))))) |
55 | 54 | ralrimiva 2949 |
. 2
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) → ∀𝑥 ∈ Cℋ
(𝑥 ⊆ (𝐵 ∩ 𝐶) → ((𝑥 ∨ℋ 𝐷) ∩ (𝐵 ∩ 𝐶)) ⊆ (𝑥 ∨ℋ (𝐷 ∩ (𝐵 ∩ 𝐶))))) |
56 | 14, 22 | chincli 27703 |
. . 3
⊢ (𝐵 ∩ 𝐶) ∈
Cℋ |
57 | | mdbr2 28539 |
. . 3
⊢ ((𝐷 ∈
Cℋ ∧ (𝐵 ∩ 𝐶) ∈ Cℋ )
→ (𝐷
𝑀ℋ (𝐵 ∩ 𝐶) ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ (𝐵 ∩ 𝐶) → ((𝑥 ∨ℋ 𝐷) ∩ (𝐵 ∩ 𝐶)) ⊆ (𝑥 ∨ℋ (𝐷 ∩ (𝐵 ∩ 𝐶)))))) |
58 | 1, 56, 57 | mp2an 704 |
. 2
⊢ (𝐷 𝑀ℋ
(𝐵 ∩ 𝐶) ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ (𝐵 ∩ 𝐶) → ((𝑥 ∨ℋ 𝐷) ∩ (𝐵 ∩ 𝐶)) ⊆ (𝑥 ∨ℋ (𝐷 ∩ (𝐵 ∩ 𝐶))))) |
59 | 55, 58 | sylibr 223 |
1
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ (𝐴 ∩ 𝐵) 𝑀ℋ 𝐶) ∧ ((𝐴 ∩ 𝐶) ⊆ 𝐷 ∧ 𝐷 ⊆ 𝐴)) → 𝐷 𝑀ℋ (𝐵 ∩ 𝐶)) |