Step | Hyp | Ref
| Expression |
1 | | mdexch.3 |
. . . . . . . . . . . . . . 15
⊢ 𝐶 ∈
Cℋ |
2 | | mdexch.1 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 ∈
Cℋ |
3 | | chjass 28392 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → ((𝐶 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐶 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
4 | 1, 2, 3 | mp3an12 1414 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → ((𝐶 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐶 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
5 | 1, 2 | chjcli 28316 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∨ℋ 𝐴) ∈
Cℋ |
6 | | chjcom 28365 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∨ℋ 𝐴) ∈ Cℋ )
→ (𝑥
∨ℋ (𝐶
∨ℋ 𝐴))
= ((𝐶
∨ℋ 𝐴)
∨ℋ 𝑥)) |
7 | 5, 6 | mpan2 707 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) = ((𝐶 ∨ℋ 𝐴) ∨ℋ 𝑥)) |
8 | | chjcl 28216 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) |
9 | 2, 8 | mpan 706 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → (𝐴 ∨ℋ 𝑥) ∈ Cℋ
) |
10 | | chjcom 28365 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∨ℋ 𝑥) ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐴
∨ℋ 𝑥)
∨ℋ 𝐶) =
(𝐶 ∨ℋ
(𝐴 ∨ℋ
𝑥))) |
11 | 9, 1, 10 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) = (𝐶 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
12 | 4, 7, 11 | 3eqtr4d 2666 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶)) |
13 | 12 | ineq1d 3813 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ 𝐵)) |
14 | | inass 3823 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) |
15 | | incom 3805 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) = (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) |
16 | | mdexch.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐵 ∈
Cℋ |
17 | 2, 16 | chjcomi 28327 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) |
18 | 17 | ineq2i 3811 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = (𝐵 ∩ (𝐵 ∨ℋ 𝐴)) |
19 | 16, 2 | chabs2i 28378 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∩ (𝐵 ∨ℋ 𝐴)) = 𝐵 |
20 | 18, 19 | eqtri 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐵 |
21 | 15, 20 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) = 𝐵 |
22 | 21 | ineq2i 3811 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ 𝐵) |
23 | 14, 22 | eqtri 2644 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ 𝐵) |
24 | 13, 23 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) = ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵)) |
25 | 24 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) = ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵)) |
26 | | chlej2 28370 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) ∧ 𝑥 ⊆ 𝐵) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵)) |
27 | 26 | ex 450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) → (𝑥 ⊆ 𝐵 → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
28 | 16, 2, 27 | mp3an23 1416 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) |
29 | 2, 16 | chjcli 28316 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∨ℋ 𝐵) ∈
Cℋ |
30 | | mdi 29154 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
31 | 30 | exp32 631 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) |
32 | 1, 29, 31 | mp3an12 1414 |
. . . . . . . . . . . . . . . . 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 448 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵)) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
37 | 36 | adantrr 753 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
38 | 1, 29 | chincli 28319 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∈
Cℋ |
39 | | chlej2 28370 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ )
∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴)) |
40 | 39 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ )
→ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴))) |
41 | 38, 2, 40 | mp3an12 1414 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∨ℋ 𝑥) ∈
Cℋ → ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴))) |
42 | 9, 41 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴))) |
43 | 42 | imp 445 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴)) |
44 | | chjcom 28365 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∨ℋ 𝑥) ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ ((𝐴
∨ℋ 𝑥)
∨ℋ 𝐴) =
(𝐴 ∨ℋ
(𝐴 ∨ℋ
𝑥))) |
45 | 9, 2, 44 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴) = (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
46 | 2 | chjidmi 28380 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∨ℋ 𝐴) = 𝐴 |
47 | 46 | oveq1i 6660 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐴 ∨ℋ 𝑥) |
48 | | chjass 28392 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → ((𝐴 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
49 | 2, 2, 48 | mp3an12 1414 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥))) |
50 | | chjcom 28365 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐴
∨ℋ 𝑥) =
(𝑥 ∨ℋ
𝐴)) |
51 | 2, 50 | mpan 706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
Cℋ → (𝐴 ∨ℋ 𝑥) = (𝑥 ∨ℋ 𝐴)) |
52 | 47, 49, 51 | 3eqtr3a 2680 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥)) = (𝑥 ∨ℋ 𝐴)) |
53 | 45, 52 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴) = (𝑥 ∨ℋ 𝐴)) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴) = (𝑥 ∨ℋ 𝐴)) |
55 | 43, 54 | sseqtrd 3641 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ (𝑥 ∨ℋ 𝐴)) |
56 | 55 | ad2ant2rl 785 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ (𝑥 ∨ℋ 𝐴)) |
57 | 37, 56 | eqsstrd 3639 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝑥 ∨ℋ 𝐴)) |
58 | | ssrin 3838 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝑥 ∨ℋ 𝐴) → ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) |
59 | 57, 58 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) |
60 | 25, 59 | eqsstrd 3639 |
. . . . . . . . 9
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) |
61 | 60 | adantrl 752 |
. . . . . . . 8
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴))) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) |
62 | | mdi 29154 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵)) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) |
63 | 62 | exp32 631 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → (𝐴 𝑀ℋ 𝐵 → (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |
64 | 2, 16, 63 | mp3an12 1414 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → (𝐴 𝑀ℋ 𝐵 → (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |
65 | 64 | com23 86 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → (𝐴 𝑀ℋ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |
66 | 65 | imp31 448 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐴 𝑀ℋ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) |
67 | 2, 1 | chub2i 28329 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐶 ∨ℋ 𝐴) |
68 | | ssrin 3838 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ (𝐶 ∨ℋ 𝐴) → (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)) |
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) |
70 | 2, 16 | chincli 28319 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ 𝐵) ∈
Cℋ |
71 | 5, 16 | chincli 28319 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) ∈
Cℋ |
72 | | chlej2 28370 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∩ 𝐵) ∈ Cℋ
∧ ((𝐶
∨ℋ 𝐴)
∩ 𝐵) ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
∧ (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
73 | 72 | ex 450 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∩ 𝐵) ∈ Cℋ
∧ ((𝐶
∨ℋ 𝐴)
∩ 𝐵) ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ ((𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) |
74 | 70, 71, 73 | mp3an12 1414 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) |
75 | 69, 74 | mpi 20 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
76 | 75 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐴 𝑀ℋ 𝐵) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
77 | 66, 76 | eqsstrd 3639 |
. . . . . . . . 9
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐴 𝑀ℋ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
78 | 77 | adantrr 753 |
. . . . . . . 8
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴))) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
79 | 61, 78 | sstrd 3613 |
. . . . . . 7
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴))) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) |
80 | 79 | exp31 630 |
. . . . . 6
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → ((𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) |
81 | 80 | com3r 87 |
. . . . 5
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → (𝑥 ∈ Cℋ
→ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) |
82 | 81 | 3impb 1260 |
. . . 4
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → (𝑥 ∈ Cℋ
→ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) |
83 | 82 | ralrimiv 2965 |
. . 3
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) |
84 | | mdbr2 29155 |
. . . 4
⊢ (((𝐶 ∨ℋ 𝐴) ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((𝐶
∨ℋ 𝐴)
𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) |
85 | 5, 16, 84 | mp2an 708 |
. . 3
⊢ ((𝐶 ∨ℋ 𝐴) 𝑀ℋ
𝐵 ↔ ∀𝑥 ∈
Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) |
86 | 83, 85 | sylibr 224 |
. 2
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → (𝐶 ∨ℋ 𝐴) 𝑀ℋ 𝐵) |
87 | 1, 2 | chjcomi 28327 |
. . . . 5
⊢ (𝐶 ∨ℋ 𝐴) = (𝐴 ∨ℋ 𝐶) |
88 | | incom 3805 |
. . . . . 6
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) |
89 | 18, 88, 19 | 3eqtr3ri 2653 |
. . . . 5
⊢ 𝐵 = ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) |
90 | 87, 89 | ineq12i 3812 |
. . . 4
⊢ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = ((𝐴 ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) |
91 | | inass 3823 |
. . . . 5
⊢ (((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = ((𝐴 ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) |
92 | 2, 16 | chub1i 28328 |
. . . . . . . 8
⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵) |
93 | | mdi 29154 |
. . . . . . . . . 10
⊢ (((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
94 | 93 | exp32 631 |
. . . . . . . . 9
⊢ ((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → (𝐴 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) |
95 | 1, 29, 2, 94 | mp3an 1424 |
. . . . . . . 8
⊢ (𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) → (𝐴 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))))) |
96 | 92, 95 | mpi 20 |
. . . . . . 7
⊢ (𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) |
97 | 2, 38 | chjcomi 28327 |
. . . . . . . 8
⊢ (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) = ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐴) |
98 | 38, 2 | chlejb1i 28335 |
. . . . . . . . 9
⊢ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 ↔ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐴) = 𝐴) |
99 | 98 | biimpi 206 |
. . . . . . . 8
⊢ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐴) = 𝐴) |
100 | 97, 99 | syl5eq 2668 |
. . . . . . 7
⊢ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) = 𝐴) |
101 | 96, 100 | sylan9eq 2676 |
. . . . . 6
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴) |
102 | 101 | ineq1d 3813 |
. . . . 5
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → (((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = (𝐴 ∩ 𝐵)) |
103 | 91, 102 | syl5eqr 2670 |
. . . 4
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) = (𝐴 ∩ 𝐵)) |
104 | 90, 103 | syl5eq 2668 |
. . 3
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵)) |
105 | 104 | 3adant1 1079 |
. 2
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵)) |
106 | 86, 105 | jca 554 |
1
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) 𝑀ℋ 𝐵 ∧ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵))) |