Step | Hyp | Ref
| Expression |
1 | | ineq2 4140 |
. . . . . . 7
⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) → (𝑥 ∩ (𝐴 +ℋ 𝐵)) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))) |
2 | 1 | adantr 481 |
. . . . . 6
⊢ (((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ∧ (𝑥 ∈ Cℋ
∧ 𝐵 ⊆ 𝑥)) → (𝑥 ∩ (𝐴 +ℋ 𝐵)) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))) |
3 | | elin 3903 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑥 ∩ (𝐴 +ℋ 𝐵)) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ (𝐴 +ℋ 𝐵))) |
4 | | sumdmdi.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈
Cℋ |
5 | | sumdmdi.2 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈
Cℋ |
6 | 4, 5 | chseli 29821 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤)) |
7 | | ssel2 3916 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ⊆ 𝑥 ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ 𝑥) |
8 | | chsh 29586 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈
Cℋ → 𝑥 ∈ Sℋ
) |
9 | | shsubcl 29582 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈
Sℋ ∧ 𝑦 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (𝑦 −ℎ 𝑤) ∈ 𝑥) |
10 | 9 | 3exp 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈
Sℋ → (𝑦 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑦 −ℎ 𝑤) ∈ 𝑥))) |
11 | 8, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈
Cℋ → (𝑦 ∈ 𝑥 → (𝑤 ∈ 𝑥 → (𝑦 −ℎ 𝑤) ∈ 𝑥))) |
12 | 7, 11 | syl7 74 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈
Cℋ → (𝑦 ∈ 𝑥 → ((𝐵 ⊆ 𝑥 ∧ 𝑤 ∈ 𝐵) → (𝑦 −ℎ 𝑤) ∈ 𝑥))) |
13 | 12 | exp4a 432 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈
Cℋ → (𝑦 ∈ 𝑥 → (𝐵 ⊆ 𝑥 → (𝑤 ∈ 𝐵 → (𝑦 −ℎ 𝑤) ∈ 𝑥)))) |
14 | 13 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈
Cℋ → (𝐵 ⊆ 𝑥 → (𝑦 ∈ 𝑥 → (𝑤 ∈ 𝐵 → (𝑦 −ℎ 𝑤) ∈ 𝑥)))) |
15 | 14 | imp41 426 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑤 ∈ 𝐵) → (𝑦 −ℎ 𝑤) ∈ 𝑥) |
16 | 15 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝑦 −ℎ 𝑤) ∈ 𝑥) |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑦 = (𝑧 +ℎ 𝑤)) → (𝑦 −ℎ 𝑤) ∈ 𝑥) |
18 | | chel 29592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈
Cℋ ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ℋ) |
19 | 18 | adantlr 712 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ ℋ) |
20 | 4 | cheli 29594 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ ℋ) |
21 | 5 | cheli 29594 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ 𝐵 → 𝑤 ∈ ℋ) |
22 | | hvsubadd 29439 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 −ℎ
𝑤) = 𝑧 ↔ (𝑤 +ℎ 𝑧) = 𝑦)) |
23 | | ax-hvcom 29363 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑤 +ℎ 𝑧) = (𝑧 +ℎ 𝑤)) |
24 | 23 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑤 +ℎ 𝑧) = 𝑦 ↔ (𝑧 +ℎ 𝑤) = 𝑦)) |
25 | | eqcom 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑧 +ℎ 𝑤) = 𝑦 ↔ 𝑦 = (𝑧 +ℎ 𝑤)) |
26 | 24, 25 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑤 +ℎ 𝑧) = 𝑦 ↔ 𝑦 = (𝑧 +ℎ 𝑤))) |
27 | 26 | 3adant1 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑤 +ℎ 𝑧) = 𝑦 ↔ 𝑦 = (𝑧 +ℎ 𝑤))) |
28 | 22, 27 | bitrd 278 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℋ ∧ 𝑤 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 −ℎ
𝑤) = 𝑧 ↔ 𝑦 = (𝑧 +ℎ 𝑤))) |
29 | 28 | 3com23 1125 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ ∧ 𝑤 ∈ ℋ) → ((𝑦 −ℎ
𝑤) = 𝑧 ↔ 𝑦 = (𝑧 +ℎ 𝑤))) |
30 | 19, 20, 21, 29 | syl3an 1159 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → ((𝑦 −ℎ 𝑤) = 𝑧 ↔ 𝑦 = (𝑧 +ℎ 𝑤))) |
31 | 30 | 3expa 1117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → ((𝑦 −ℎ 𝑤) = 𝑧 ↔ 𝑦 = (𝑧 +ℎ 𝑤))) |
32 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 −ℎ
𝑤) = 𝑧 → ((𝑦 −ℎ 𝑤) ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
33 | 31, 32 | syl6bir 253 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) → (𝑦 = (𝑧 +ℎ 𝑤) → ((𝑦 −ℎ 𝑤) ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))) |
34 | 33 | imp 407 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑦 = (𝑧 +ℎ 𝑤)) → ((𝑦 −ℎ 𝑤) ∈ 𝑥 ↔ 𝑧 ∈ 𝑥)) |
35 | 17, 34 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑦 = (𝑧 +ℎ 𝑤)) → 𝑧 ∈ 𝑥) |
36 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑦 = (𝑧 +ℎ 𝑤)) → 𝑦 = (𝑧 +ℎ 𝑤)) |
37 | 35, 36 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) ∧ 𝑤 ∈ 𝐵) ∧ 𝑦 = (𝑧 +ℎ 𝑤)) → (𝑧 ∈ 𝑥 ∧ 𝑦 = (𝑧 +ℎ 𝑤))) |
38 | 37 | exp31 420 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) → (𝑤 ∈ 𝐵 → (𝑦 = (𝑧 +ℎ 𝑤) → (𝑧 ∈ 𝑥 ∧ 𝑦 = (𝑧 +ℎ 𝑤))))) |
39 | 38 | reximdvai 3200 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) → (∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤) → ∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑥 ∧ 𝑦 = (𝑧 +ℎ 𝑤)))) |
40 | | r19.42v 3279 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑤 ∈
𝐵 (𝑧 ∈ 𝑥 ∧ 𝑦 = (𝑧 +ℎ 𝑤)) ↔ (𝑧 ∈ 𝑥 ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤))) |
41 | 39, 40 | syl6ib 250 |
. . . . . . . . . . . . . 14
⊢ ((((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝐴) → (∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤) → (𝑧 ∈ 𝑥 ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤)))) |
42 | 41 | reximdva 3203 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤) → ∃𝑧 ∈ 𝐴 (𝑧 ∈ 𝑥 ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤)))) |
43 | | elin 3903 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ (𝑥 ∩ 𝐴) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴)) |
44 | | ancom 461 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥)) |
45 | 43, 44 | bitri 274 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝑥 ∩ 𝐴) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥)) |
46 | 45 | anbi1i 624 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ (𝑥 ∩ 𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤))) |
47 | | anass 469 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ (𝑧 ∈ 𝑥 ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤)))) |
48 | 46, 47 | bitri 274 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ (𝑥 ∩ 𝐴) ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤)) ↔ (𝑧 ∈ 𝐴 ∧ (𝑧 ∈ 𝑥 ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤)))) |
49 | 48 | rexbii2 3179 |
. . . . . . . . . . . . 13
⊢
(∃𝑧 ∈
(𝑥 ∩ 𝐴)∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤) ↔ ∃𝑧 ∈ 𝐴 (𝑧 ∈ 𝑥 ∧ ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤))) |
50 | 42, 49 | syl6ibr 251 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤) → ∃𝑧 ∈ (𝑥 ∩ 𝐴)∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤))) |
51 | 4 | chshii 29589 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 ∈
Sℋ |
52 | | shincl 29743 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈
Sℋ ∧ 𝐴 ∈ Sℋ )
→ (𝑥 ∩ 𝐴) ∈
Sℋ ) |
53 | 8, 51, 52 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → (𝑥 ∩ 𝐴) ∈ Sℋ
) |
54 | 53 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) → (𝑥 ∩ 𝐴) ∈ Sℋ
) |
55 | 5 | chshii 29589 |
. . . . . . . . . . . . 13
⊢ 𝐵 ∈
Sℋ |
56 | | shsel 29676 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∩ 𝐴) ∈ Sℋ
∧ 𝐵 ∈
Sℋ ) → (𝑦 ∈ ((𝑥 ∩ 𝐴) +ℋ 𝐵) ↔ ∃𝑧 ∈ (𝑥 ∩ 𝐴)∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤))) |
57 | 54, 55, 56 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∈ ((𝑥 ∩ 𝐴) +ℋ 𝐵) ↔ ∃𝑧 ∈ (𝑥 ∩ 𝐴)∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤))) |
58 | 50, 57 | sylibrd 258 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑦 = (𝑧 +ℎ 𝑤) → 𝑦 ∈ ((𝑥 ∩ 𝐴) +ℋ 𝐵))) |
59 | 6, 58 | syl5bi 241 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∈ (𝐴 +ℋ 𝐵) → 𝑦 ∈ ((𝑥 ∩ 𝐴) +ℋ 𝐵))) |
60 | 59 | expimpd 454 |
. . . . . . . . 9
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) → ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ (𝐴 +ℋ 𝐵)) → 𝑦 ∈ ((𝑥 ∩ 𝐴) +ℋ 𝐵))) |
61 | 3, 60 | syl5bi 241 |
. . . . . . . 8
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) → (𝑦 ∈ (𝑥 ∩ (𝐴 +ℋ 𝐵)) → 𝑦 ∈ ((𝑥 ∩ 𝐴) +ℋ 𝐵))) |
62 | 61 | ssrdv 3927 |
. . . . . . 7
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ⊆ 𝑥) → (𝑥 ∩ (𝐴 +ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) +ℋ 𝐵)) |
63 | 62 | adantl 482 |
. . . . . 6
⊢ (((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ∧ (𝑥 ∈ Cℋ
∧ 𝐵 ⊆ 𝑥)) → (𝑥 ∩ (𝐴 +ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) +ℋ 𝐵)) |
64 | 2, 63 | eqsstrrd 3960 |
. . . . 5
⊢ (((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ∧ (𝑥 ∈ Cℋ
∧ 𝐵 ⊆ 𝑥)) → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) +ℋ 𝐵)) |
65 | | chincl 29861 |
. . . . . . . 8
⊢ ((𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (𝑥 ∩ 𝐴) ∈
Cℋ ) |
66 | 4, 65 | mpan2 688 |
. . . . . . 7
⊢ (𝑥 ∈
Cℋ → (𝑥 ∩ 𝐴) ∈ Cℋ
) |
67 | | chslej 29860 |
. . . . . . 7
⊢ (((𝑥 ∩ 𝐴) ∈ Cℋ
∧ 𝐵 ∈
Cℋ ) → ((𝑥 ∩ 𝐴) +ℋ 𝐵) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)) |
68 | 66, 5, 67 | sylancl 586 |
. . . . . 6
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∩ 𝐴) +ℋ 𝐵) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)) |
69 | 68 | ad2antrl 725 |
. . . . 5
⊢ (((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ∧ (𝑥 ∈ Cℋ
∧ 𝐵 ⊆ 𝑥)) → ((𝑥 ∩ 𝐴) +ℋ 𝐵) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)) |
70 | 64, 69 | sstrd 3931 |
. . . 4
⊢ (((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ∧ (𝑥 ∈ Cℋ
∧ 𝐵 ⊆ 𝑥)) → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)) |
71 | 70 | exp32 421 |
. . 3
⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) → (𝑥 ∈ Cℋ
→ (𝐵 ⊆ 𝑥 → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)))) |
72 | 71 | ralrimiv 3102 |
. 2
⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) → ∀𝑥 ∈ Cℋ
(𝐵 ⊆ 𝑥 → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵))) |
73 | | dmdbr2 30665 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ
(𝐵 ⊆ 𝑥 → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)))) |
74 | 4, 5, 73 | mp2an 689 |
. 2
⊢ (𝐴
𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ
(𝐵 ⊆ 𝑥 → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵))) |
75 | 72, 74 | sylibr 233 |
1
⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) → 𝐴 𝑀ℋ*
𝐵) |