Step | Hyp | Ref
| Expression |
1 | | mdexch.3 |
. . . . . . . . . . . . . . 15
⊢ 𝐶 ∈
Cℋ |
2 | | mdexch.1 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 ∈
Cℋ |
3 | | chjass 29891 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → ((𝐶 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐶 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
4 | 1, 2, 3 | mp3an12 1450 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → ((𝐶 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐶 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
5 | 1, 2 | chjcli 29815 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∨ℋ 𝐴) ∈
Cℋ |
6 | | chjcom 29864 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∨ℋ 𝐴) ∈ Cℋ )
→ (𝑥
∨ℋ (𝐶
∨ℋ 𝐴))
= ((𝐶
∨ℋ 𝐴)
∨ℋ 𝑥)) |
7 | 5, 6 | mpan2 688 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) = ((𝐶 ∨ℋ 𝐴) ∨ℋ 𝑥)) |
8 | | chjcl 29715 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) |
9 | 2, 8 | mpan 687 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → (𝐴 ∨ℋ 𝑥) ∈ Cℋ
) |
10 | | chjcom 29864 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∨ℋ 𝑥) ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐴
∨ℋ 𝑥)
∨ℋ 𝐶) =
(𝐶 ∨ℋ
(𝐴 ∨ℋ
𝑥))) |
11 | 9, 1, 10 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) = (𝐶 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
12 | 4, 7, 11 | 3eqtr4d 2790 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶)) |
13 | 12 | ineq1d 4151 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ 𝐵)) |
14 | | inass 4159 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) |
15 | | incom 4140 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) = (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) |
16 | | mdexch.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐵 ∈
Cℋ |
17 | 2, 16 | chjcomi 29826 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) |
18 | 17 | ineq2i 4149 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = (𝐵 ∩ (𝐵 ∨ℋ 𝐴)) |
19 | 16, 2 | chabs2i 29877 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∩ (𝐵 ∨ℋ 𝐴)) = 𝐵 |
20 | 18, 19 | eqtri 2768 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐵 |
21 | 15, 20 | eqtri 2768 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) = 𝐵 |
22 | 21 | ineq2i 4149 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ 𝐵) |
23 | 14, 22 | eqtri 2768 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ 𝐵) |
24 | 13, 23 | eqtr4di 2798 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) = ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵)) |
25 | 24 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) = ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵)) |
26 | | chlej2 29869 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) ∧ 𝑥 ⊆ 𝐵) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵)) |
27 | 26 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) → (𝑥 ⊆ 𝐵 → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
28 | 16, 2, 27 | mp3an23 1452 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
29 | 2, 16 | chjcli 29815 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∨ℋ 𝐵) ∈
Cℋ |
30 | | mdi 30653 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
31 | 30 | exp32 421 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) |
32 | 1, 29, 31 | mp3an12 1450 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∨ℋ 𝑥) ∈
Cℋ → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) |
33 | 9, 32 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) |
34 | 33 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵) → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) |
35 | 28, 34 | syld 47 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) |
36 | 35 | imp31 418 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵)) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
37 | 36 | adantrr 714 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
38 | 1, 29 | chincli 29818 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∈
Cℋ |
39 | | chlej2 29869 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ )
∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴)) |
40 | 39 | ex 413 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ )
→ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴))) |
41 | 38, 2, 40 | mp3an12 1450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∨ℋ 𝑥) ∈
Cℋ → ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴))) |
42 | 9, 41 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴))) |
43 | 42 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴)) |
44 | | chjcom 29864 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∨ℋ 𝑥) ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ ((𝐴
∨ℋ 𝑥)
∨ℋ 𝐴) =
(𝐴 ∨ℋ
(𝐴 ∨ℋ
𝑥))) |
45 | 9, 2, 44 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴) = (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
46 | 2 | chjidmi 29879 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∨ℋ 𝐴) = 𝐴 |
47 | 46 | oveq1i 7281 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐴 ∨ℋ 𝑥) |
48 | | chjass 29891 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → ((𝐴 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
49 | 2, 2, 48 | mp3an12 1450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
50 | | chjcom 29864 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐴
∨ℋ 𝑥) =
(𝑥 ∨ℋ
𝐴)) |
51 | 2, 50 | mpan 687 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
Cℋ → (𝐴 ∨ℋ 𝑥) = (𝑥 ∨ℋ 𝐴)) |
52 | 47, 49, 51 | 3eqtr3a 2804 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥)) = (𝑥 ∨ℋ 𝐴)) |
53 | 45, 52 | eqtrd 2780 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴) = (𝑥 ∨ℋ 𝐴)) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴) = (𝑥 ∨ℋ 𝐴)) |
55 | 43, 54 | sseqtrd 3966 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ (𝑥 ∨ℋ 𝐴)) |
56 | 55 | ad2ant2rl 746 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ (𝑥 ∨ℋ 𝐴)) |
57 | 37, 56 | eqsstrd 3964 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝑥 ∨ℋ 𝐴)) |
58 | 57 | ssrind 4175 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) |
59 | 25, 58 | eqsstrd 3964 |
. . . . . . . . 9
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) |
60 | 59 | adantrl 713 |
. . . . . . . 8
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴))) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) |
61 | | mdi 30653 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵)) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) |
62 | 61 | exp32 421 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → (𝐴 𝑀ℋ 𝐵 → (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |
63 | 2, 16, 62 | mp3an12 1450 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → (𝐴 𝑀ℋ 𝐵 → (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |
64 | 63 | com23 86 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → (𝐴 𝑀ℋ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |
65 | 64 | imp31 418 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐴 𝑀ℋ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) |
66 | 2, 1 | chub2i 29828 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐶 ∨ℋ 𝐴) |
67 | | ssrin 4173 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ (𝐶 ∨ℋ 𝐴) → (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) |
69 | 2, 16 | chincli 29818 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ 𝐵) ∈
Cℋ |
70 | 5, 16 | chincli 29818 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) ∈
Cℋ |
71 | | chlej2 29869 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∩ 𝐵) ∈ Cℋ
∧ ((𝐶
∨ℋ 𝐴)
∩ 𝐵) ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
∧ (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
72 | 71 | ex 413 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∩ 𝐵) ∈ Cℋ
∧ ((𝐶
∨ℋ 𝐴)
∩ 𝐵) ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ ((𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) |
73 | 69, 70, 72 | mp3an12 1450 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) |
74 | 68, 73 | mpi 20 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
75 | 74 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐴 𝑀ℋ 𝐵) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
76 | 65, 75 | eqsstrd 3964 |
. . . . . . . . 9
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐴 𝑀ℋ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
77 | 76 | adantrr 714 |
. . . . . . . 8
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴))) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
78 | 60, 77 | sstrd 3936 |
. . . . . . 7
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴))) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
79 | 78 | exp31 420 |
. . . . . 6
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → ((𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) |
80 | 79 | com3r 87 |
. . . . 5
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → (𝑥 ∈ Cℋ
→ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) |
81 | 80 | 3impb 1114 |
. . . 4
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → (𝑥 ∈ Cℋ
→ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) |
82 | 81 | ralrimiv 3109 |
. . 3
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) |
83 | | mdbr2 30654 |
. . . 4
⊢ (((𝐶 ∨ℋ 𝐴) ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((𝐶
∨ℋ 𝐴)
𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) |
84 | 5, 16, 83 | mp2an 689 |
. . 3
⊢ ((𝐶 ∨ℋ 𝐴) 𝑀ℋ
𝐵 ↔ ∀𝑥 ∈
Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) |
85 | 82, 84 | sylibr 233 |
. 2
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → (𝐶 ∨ℋ 𝐴) 𝑀ℋ 𝐵) |
86 | 1, 2 | chjcomi 29826 |
. . . . 5
⊢ (𝐶 ∨ℋ 𝐴) = (𝐴 ∨ℋ 𝐶) |
87 | | incom 4140 |
. . . . . 6
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) |
88 | 18, 87, 19 | 3eqtr3ri 2777 |
. . . . 5
⊢ 𝐵 = ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) |
89 | 86, 88 | ineq12i 4150 |
. . . 4
⊢ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = ((𝐴 ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) |
90 | | inass 4159 |
. . . . 5
⊢ (((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = ((𝐴 ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) |
91 | 2, 16 | chub1i 29827 |
. . . . . . . 8
⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵) |
92 | | mdi 30653 |
. . . . . . . . . 10
⊢ (((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
93 | 92 | exp32 421 |
. . . . . . . . 9
⊢ ((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → (𝐴 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) |
94 | 1, 29, 2, 93 | mp3an 1460 |
. . . . . . . 8
⊢ (𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) → (𝐴 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))))) |
95 | 91, 94 | mpi 20 |
. . . . . . 7
⊢ (𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
96 | 2, 38 | chjcomi 29826 |
. . . . . . . 8
⊢ (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) = ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐴) |
97 | 38, 2 | chlejb1i 29834 |
. . . . . . . . 9
⊢ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 ↔ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐴) = 𝐴) |
98 | 97 | biimpi 215 |
. . . . . . . 8
⊢ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐴) = 𝐴) |
99 | 96, 98 | eqtrid 2792 |
. . . . . . 7
⊢ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) = 𝐴) |
100 | 95, 99 | sylan9eq 2800 |
. . . . . 6
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴) |
101 | 100 | ineq1d 4151 |
. . . . 5
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → (((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = (𝐴 ∩ 𝐵)) |
102 | 90, 101 | eqtr3id 2794 |
. . . 4
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) = (𝐴 ∩ 𝐵)) |
103 | 89, 102 | eqtrid 2792 |
. . 3
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵)) |
104 | 103 | 3adant1 1129 |
. 2
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵)) |
105 | 85, 104 | jca 512 |
1
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) 𝑀ℋ 𝐵 ∧ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵))) |