Proof of Theorem dmdbr5ati
Step | Hyp | Ref
| Expression |
1 | | atelch 28587 |
. . . . . 6
⊢ (𝑥 ∈ HAtoms → 𝑥 ∈
Cℋ ) |
2 | | sumdmdi.1 |
. . . . . . . 8
⊢ 𝐴 ∈
Cℋ |
3 | | sumdmdi.2 |
. . . . . . . 8
⊢ 𝐵 ∈
Cℋ |
4 | | dmdi4 28550 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → (𝐴 𝑀ℋ*
𝐵 → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
5 | 2, 3, 4 | mp3an12 1406 |
. . . . . . 7
⊢ (𝑥 ∈
Cℋ → (𝐴 𝑀ℋ*
𝐵 → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
6 | 5 | com12 32 |
. . . . . 6
⊢ (𝐴
𝑀ℋ* 𝐵 → (𝑥 ∈ Cℋ
→ ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵))) |
7 | 1, 6 | syl5 33 |
. . . . 5
⊢ (𝐴
𝑀ℋ* 𝐵 → (𝑥 ∈ HAtoms → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
8 | 7 | a1dd 48 |
. . . 4
⊢ (𝐴
𝑀ℋ* 𝐵 → (𝑥 ∈ HAtoms → (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
9 | 8 | ralrimiv 2948 |
. . 3
⊢ (𝐴
𝑀ℋ* 𝐵 → ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
10 | | chjcom 27749 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐵
∨ℋ 𝑥) =
(𝑥 ∨ℋ
𝐵)) |
11 | 3, 1, 10 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ HAtoms → (𝐵 ∨ℋ 𝑥) = (𝑥 ∨ℋ 𝐵)) |
12 | 11 | ineq1d 3775 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ HAtoms → ((𝐵 ∨ℋ 𝑥) ∩ (𝐵 ∨ℋ 𝐴)) = ((𝑥 ∨ℋ 𝐵) ∩ (𝐵 ∨ℋ 𝐴))) |
13 | 2, 3 | chjcomi 27711 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) |
14 | 13 | ineq2i 3773 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝑥 ∨ℋ 𝐵) ∩ (𝐵 ∨ℋ 𝐴)) |
15 | 12, 14 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ HAtoms → ((𝐵 ∨ℋ 𝑥) ∩ (𝐵 ∨ℋ 𝐴)) = ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
16 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝐵 ∨ℋ 𝑥) ∩ (𝐵 ∨ℋ 𝐴)) = ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
17 | 13 | sseq2i 3593 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ↔ 𝑥 ⊆ (𝐵 ∨ℋ 𝐴)) |
18 | 17 | notbii 309 |
. . . . . . . . . . . 12
⊢ (¬
𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ↔ ¬ 𝑥 ⊆ (𝐵 ∨ℋ 𝐴)) |
19 | 3, 2 | atabs2i 28645 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ HAtoms → (¬
𝑥 ⊆ (𝐵 ∨ℋ 𝐴) → ((𝐵 ∨ℋ 𝑥) ∩ (𝐵 ∨ℋ 𝐴)) = 𝐵)) |
20 | 19 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ (𝐵 ∨ℋ 𝐴)) → ((𝐵 ∨ℋ 𝑥) ∩ (𝐵 ∨ℋ 𝐴)) = 𝐵) |
21 | 18, 20 | sylan2b 491 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝐵 ∨ℋ 𝑥) ∩ (𝐵 ∨ℋ 𝐴)) = 𝐵) |
22 | 16, 21 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) = 𝐵) |
23 | | chjcl 27600 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑥
∨ℋ 𝐵)
∈ Cℋ ) |
24 | 1, 3, 23 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ HAtoms → (𝑥 ∨ℋ 𝐵) ∈
Cℋ ) |
25 | | chincl 27742 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∨ℋ 𝐵) ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ ((𝑥
∨ℋ 𝐵)
∩ 𝐴) ∈
Cℋ ) |
26 | 24, 2, 25 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ HAtoms → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∈ Cℋ
) |
27 | | chub2 27751 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈
Cℋ ∧ ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∈ Cℋ )
→ 𝐵 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
28 | 3, 26, 27 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ HAtoms → 𝐵 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
29 | 28 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → 𝐵 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
30 | 22, 29 | eqsstrd 3602 |
. . . . . . . . 9
⊢ ((𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
31 | 30 | ex 449 |
. . . . . . . 8
⊢ (𝑥 ∈ HAtoms → (¬
𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
32 | 31 | biantrud 527 |
. . . . . . 7
⊢ (𝑥 ∈ HAtoms → ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ∧ (¬ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))))) |
33 | | pm4.83 966 |
. . . . . . 7
⊢ (((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ∧ (¬ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) ↔ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
34 | 32, 33 | syl6bb 275 |
. . . . . 6
⊢ (𝑥 ∈ HAtoms → ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
35 | 34 | ralbiia 2962 |
. . . . 5
⊢
(∀𝑥 ∈
HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ ∀𝑥 ∈ HAtoms ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
36 | 2, 3 | sumdmdlem2 28662 |
. . . . 5
⊢
(∀𝑥 ∈
HAtoms ((𝑥
∨ℋ 𝐵)
∩ (𝐴
∨ℋ 𝐵))
⊆ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
→ (𝐴
+ℋ 𝐵) =
(𝐴 ∨ℋ
𝐵)) |
37 | 35, 36 | sylbi 206 |
. . . 4
⊢
(∀𝑥 ∈
HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) → (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) |
38 | 2, 3 | sumdmdi 28663 |
. . . 4
⊢ ((𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵) ↔ 𝐴 𝑀ℋ*
𝐵) |
39 | 37, 38 | sylib 207 |
. . 3
⊢
(∀𝑥 ∈
HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) → 𝐴 𝑀ℋ*
𝐵) |
40 | 9, 39 | impbii 198 |
. 2
⊢ (𝐴
𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
41 | 3, 2 | chub2i 27713 |
. . . . . . . . . . . . 13
⊢ 𝐵 ⊆ (𝐴 ∨ℋ 𝐵) |
42 | 41 | biantru 525 |
. . . . . . . . . . . 12
⊢ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ↔ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐵))) |
43 | 2, 3 | chjcli 27700 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∨ℋ 𝐵) ∈
Cℋ |
44 | | chlub 27752 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ (𝐴
∨ℋ 𝐵)
∈ Cℋ ) → ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝑥 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵))) |
45 | 3, 43, 44 | mp3an23 1408 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ∧ 𝐵 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝑥 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵))) |
46 | 42, 45 | syl5bb 271 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ↔ (𝑥 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵))) |
47 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∨ℋ 𝐵) ⊆ (𝑥 ∨ℋ 𝐵) |
48 | 47 | biantrur 526 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) ↔ ((𝑥 ∨ℋ 𝐵) ⊆ (𝑥 ∨ℋ 𝐵) ∧ (𝑥 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵))) |
49 | | ssin 3797 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∨ℋ 𝐵) ⊆ (𝑥 ∨ℋ 𝐵) ∧ (𝑥 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝑥 ∨ℋ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
50 | 48, 49 | bitri 263 |
. . . . . . . . . . 11
⊢ ((𝑥 ∨ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) ↔ (𝑥 ∨ℋ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
51 | 46, 50 | syl6bb 275 |
. . . . . . . . . 10
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) ↔ (𝑥 ∨ℋ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)))) |
52 | 51 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (𝑥 ∨ℋ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵))) |
53 | | inss1 3795 |
. . . . . . . . 9
⊢ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝑥 ∨ℋ 𝐵) |
54 | 52, 53 | jctil 558 |
. . . . . . . 8
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝑥 ∨ℋ 𝐵) ∧ (𝑥 ∨ℋ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)))) |
55 | | eqss 3583 |
. . . . . . . 8
⊢ (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) = (𝑥 ∨ℋ 𝐵) ↔ (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝑥 ∨ℋ 𝐵) ∧ (𝑥 ∨ℋ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)))) |
56 | 54, 55 | sylibr 223 |
. . . . . . 7
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) = (𝑥 ∨ℋ 𝐵)) |
57 | 56 | sseq1d 3595 |
. . . . . 6
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ↔ (𝑥 ∨ℋ 𝐵) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
58 | 3, 23 | mpan2 703 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ 𝐵) ∈ Cℋ
) |
59 | 58, 2, 25 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∈ Cℋ
) |
60 | 3, 59, 27 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑥 ∈
Cℋ → 𝐵 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) |
61 | 60 | biantrud 527 |
. . . . . . . 8
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ↔ (𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∧ 𝐵 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
62 | | chjcl 27600 |
. . . . . . . . . 10
⊢ ((((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∈ Cℋ
∧ 𝐵 ∈
Cℋ ) → (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∈ Cℋ
) |
63 | 59, 3, 62 | sylancl 693 |
. . . . . . . . 9
⊢ (𝑥 ∈
Cℋ → (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∈ Cℋ
) |
64 | | chlub 27752 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ (((𝑥
∨ℋ 𝐵)
∩ 𝐴)
∨ℋ 𝐵)
∈ Cℋ ) → ((𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∧ 𝐵 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ (𝑥 ∨ℋ 𝐵) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
65 | 3, 64 | mp3an2 1404 |
. . . . . . . . 9
⊢ ((𝑥 ∈
Cℋ ∧ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∈ Cℋ )
→ ((𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∧ 𝐵 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ (𝑥 ∨ℋ 𝐵) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
66 | 63, 65 | mpdan 699 |
. . . . . . . 8
⊢ (𝑥 ∈
Cℋ → ((𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ∧ 𝐵 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ (𝑥 ∨ℋ 𝐵) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
67 | 61, 66 | bitrd 267 |
. . . . . . 7
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ↔ (𝑥 ∨ℋ 𝐵) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
68 | 67 | adantr 480 |
. . . . . 6
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ↔ (𝑥 ∨ℋ 𝐵) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
69 | 57, 68 | bitr4d 270 |
. . . . 5
⊢ ((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ (𝐴 ∨ℋ 𝐵)) → (((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵) ↔ 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
70 | 69 | pm5.74da 719 |
. . . 4
⊢ (𝑥 ∈
Cℋ → ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
71 | 1, 70 | syl 17 |
. . 3
⊢ (𝑥 ∈ HAtoms → ((𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)))) |
72 | 71 | ralbiia 2962 |
. 2
⊢
(∀𝑥 ∈
HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝑥 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵)) ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |
73 | 40, 72 | bitri 263 |
1
⊢ (𝐴
𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ HAtoms (𝑥 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑥 ⊆ (((𝑥 ∨ℋ 𝐵) ∩ 𝐴) ∨ℋ 𝐵))) |