Step | Hyp | Ref
| Expression |
1 | | sseq1 3900 |
. . . . . . 7
⊢ (𝑦 = (⊥‘𝑥) → (𝑦 ⊆ (⊥‘𝐵) ↔ (⊥‘𝑥) ⊆ (⊥‘𝐵))) |
2 | | oveq1 7171 |
. . . . . . . . 9
⊢ (𝑦 = (⊥‘𝑥) → (𝑦 ∨ℋ (⊥‘𝐴)) = ((⊥‘𝑥) ∨ℋ
(⊥‘𝐴))) |
3 | 2 | ineq1d 4100 |
. . . . . . . 8
⊢ (𝑦 = (⊥‘𝑥) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (((⊥‘𝑥) ∨ℋ
(⊥‘𝐴)) ∩
(⊥‘𝐵))) |
4 | | oveq1 7171 |
. . . . . . . 8
⊢ (𝑦 = (⊥‘𝑥) → (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵))) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))) |
5 | 3, 4 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑦 = (⊥‘𝑥) → (((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵))) ↔
(((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵))))) |
6 | 1, 5 | imbi12d 348 |
. . . . . 6
⊢ (𝑦 = (⊥‘𝑥) → ((𝑦 ⊆ (⊥‘𝐵) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵)))) ↔
((⊥‘𝑥) ⊆
(⊥‘𝐵) →
(((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))) |
7 | 6 | rspccv 3521 |
. . . . 5
⊢
(∀𝑦 ∈
Cℋ (𝑦 ⊆ (⊥‘𝐵) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵)))) →
((⊥‘𝑥) ∈
Cℋ → ((⊥‘𝑥) ⊆ (⊥‘𝐵) → (((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))) |
8 | | choccl 29233 |
. . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → (⊥‘𝑥) ∈ Cℋ
) |
9 | 8 | imim1i 63 |
. . . . . . . . . 10
⊢
(((⊥‘𝑥)
∈ Cℋ → ((⊥‘𝑥) ⊆ (⊥‘𝐵) → (((⊥‘𝑥) ∨ℋ
(⊥‘𝐴)) ∩
(⊥‘𝐵)) =
((⊥‘𝑥)
∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵))))) → (𝑥 ∈ Cℋ
→ ((⊥‘𝑥)
⊆ (⊥‘𝐵)
→ (((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))) |
10 | 9 | com12 32 |
. . . . . . . . 9
⊢ (𝑥 ∈
Cℋ → (((⊥‘𝑥) ∈ Cℋ
→ ((⊥‘𝑥)
⊆ (⊥‘𝐵)
→ (((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))
→ ((⊥‘𝑥)
⊆ (⊥‘𝐵)
→ (((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))) |
11 | 10 | adantl 485 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → (((⊥‘𝑥) ∈ Cℋ
→ ((⊥‘𝑥)
⊆ (⊥‘𝐵)
→ (((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))
→ ((⊥‘𝑥)
⊆ (⊥‘𝐵)
→ (((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))) |
12 | | chsscon3 29427 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐵 ⊆ 𝑥 ↔ (⊥‘𝑥) ⊆ (⊥‘𝐵))) |
13 | 12 | biimpd 232 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐵 ⊆ 𝑥 → (⊥‘𝑥) ⊆ (⊥‘𝐵))) |
14 | 13 | adantll 714 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → (𝐵 ⊆ 𝑥 → (⊥‘𝑥) ⊆ (⊥‘𝐵))) |
15 | | fveq2 6668 |
. . . . . . . . . 10
⊢
((((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵))) →
(⊥‘(((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) =
(⊥‘((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵))))) |
16 | | choccl 29233 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈
Cℋ → (⊥‘𝐴) ∈ Cℋ
) |
17 | | chjcl 29284 |
. . . . . . . . . . . . . . . 16
⊢
(((⊥‘𝑥)
∈ Cℋ ∧ (⊥‘𝐴) ∈ Cℋ )
→ ((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∈ Cℋ
) |
18 | 8, 16, 17 | syl2an 599 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ ((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∈ Cℋ
) |
19 | | chdmm3 29454 |
. . . . . . . . . . . . . . 15
⊢
((((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∈ Cℋ
∧ 𝐵 ∈
Cℋ ) →
(⊥‘(((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) =
((⊥‘((⊥‘𝑥) ∨ℋ (⊥‘𝐴))) ∨ℋ 𝐵)) |
20 | 18, 19 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
∧ 𝐵 ∈
Cℋ ) →
(⊥‘(((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) =
((⊥‘((⊥‘𝑥) ∨ℋ (⊥‘𝐴))) ∨ℋ 𝐵)) |
21 | | chdmj4 29459 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (⊥‘((⊥‘𝑥) ∨ℋ (⊥‘𝐴))) = (𝑥 ∩ 𝐴)) |
22 | 21 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
∧ 𝐵 ∈
Cℋ ) → (⊥‘((⊥‘𝑥) ∨ℋ
(⊥‘𝐴))) =
(𝑥 ∩ 𝐴)) |
23 | 22 | oveq1d 7179 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
∧ 𝐵 ∈
Cℋ ) →
((⊥‘((⊥‘𝑥) ∨ℋ (⊥‘𝐴))) ∨ℋ 𝐵) = ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)) |
24 | 20, 23 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
∧ 𝐵 ∈
Cℋ ) →
(⊥‘(((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) = ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)) |
25 | 24 | anasss 470 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) →
(⊥‘(((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) = ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)) |
26 | | choccl 29233 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈
Cℋ → (⊥‘𝐵) ∈ Cℋ
) |
27 | | chincl 29426 |
. . . . . . . . . . . . . . 15
⊢
(((⊥‘𝐴)
∈ Cℋ ∧ (⊥‘𝐵) ∈ Cℋ )
→ ((⊥‘𝐴)
∩ (⊥‘𝐵))
∈ Cℋ ) |
28 | 16, 26, 27 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((⊥‘𝐴)
∩ (⊥‘𝐵))
∈ Cℋ ) |
29 | | chdmj2 29457 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ ((⊥‘𝐴) ∩ (⊥‘𝐵)) ∈ Cℋ
) → (⊥‘((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))) =
(𝑥 ∩
(⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))))) |
30 | 28, 29 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) →
(⊥‘((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))) =
(𝑥 ∩
(⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))))) |
31 | | chdmm4 29455 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))) = (𝐴 ∨ℋ 𝐵)) |
32 | 31 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) →
(⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))) = (𝐴 ∨ℋ 𝐵)) |
33 | 32 | ineq2d 4101 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) → (𝑥 ∩ (⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵)))) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))) |
34 | 30, 33 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) →
(⊥‘((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))) =
(𝑥 ∩ (𝐴 ∨ℋ 𝐵))) |
35 | 25, 34 | eqeq12d 2754 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) →
((⊥‘(((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) =
(⊥‘((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))) ↔
((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))) |
36 | 35 | ancoms 462 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) →
((⊥‘(((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) =
(⊥‘((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))) ↔
((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))) |
37 | 15, 36 | syl5ib 247 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → ((((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵))) →
((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))) |
38 | 14, 37 | imim12d 81 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → (((⊥‘𝑥) ⊆ (⊥‘𝐵) → (((⊥‘𝑥) ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))) →
(𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) |
39 | 11, 38 | syld 47 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → (((⊥‘𝑥) ∈ Cℋ
→ ((⊥‘𝑥)
⊆ (⊥‘𝐵)
→ (((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))
→ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) |
40 | 39 | ex 416 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑥 ∈
Cℋ → (((⊥‘𝑥) ∈ Cℋ
→ ((⊥‘𝑥)
⊆ (⊥‘𝐵)
→ (((⊥‘𝑥)
∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = ((⊥‘𝑥) ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))
→ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))))) |
41 | 40 | com23 86 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (((⊥‘𝑥)
∈ Cℋ → ((⊥‘𝑥) ⊆ (⊥‘𝐵) → (((⊥‘𝑥) ∨ℋ
(⊥‘𝐴)) ∩
(⊥‘𝐵)) =
((⊥‘𝑥)
∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵))))) → (𝑥 ∈ Cℋ
→ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))))) |
42 | 7, 41 | syl5 34 |
. . . 4
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ (⊥‘𝐵) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵)))) → (𝑥 ∈ Cℋ
→ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))))) |
43 | 42 | ralrimdv 3100 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ (⊥‘𝐵) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵)))) → ∀𝑥 ∈
Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) |
44 | | sseq2 3901 |
. . . . . . 7
⊢ (𝑥 = (⊥‘𝑦) → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ (⊥‘𝑦))) |
45 | | ineq1 4094 |
. . . . . . . . 9
⊢ (𝑥 = (⊥‘𝑦) → (𝑥 ∩ 𝐴) = ((⊥‘𝑦) ∩ 𝐴)) |
46 | 45 | oveq1d 7179 |
. . . . . . . 8
⊢ (𝑥 = (⊥‘𝑦) → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵)) |
47 | | ineq1 4094 |
. . . . . . . 8
⊢ (𝑥 = (⊥‘𝑦) → (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))) |
48 | 46, 47 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = (⊥‘𝑦) → (((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)) ↔ (((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵)))) |
49 | 44, 48 | imbi12d 348 |
. . . . . 6
⊢ (𝑥 = (⊥‘𝑦) → ((𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))) ↔ (𝐵 ⊆ (⊥‘𝑦) → (((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))))) |
50 | 49 | rspccv 3521 |
. . . . 5
⊢
(∀𝑥 ∈
Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))) → ((⊥‘𝑦) ∈
Cℋ → (𝐵 ⊆ (⊥‘𝑦) → (((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))))) |
51 | | choccl 29233 |
. . . . . . . . . . 11
⊢ (𝑦 ∈
Cℋ → (⊥‘𝑦) ∈ Cℋ
) |
52 | 51 | imim1i 63 |
. . . . . . . . . 10
⊢
(((⊥‘𝑦)
∈ Cℋ → (𝐵 ⊆ (⊥‘𝑦) → (((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵)))) → (𝑦 ∈ Cℋ
→ (𝐵 ⊆
(⊥‘𝑦) →
(((⊥‘𝑦) ∩
𝐴) ∨ℋ
𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))))) |
53 | 52 | com12 32 |
. . . . . . . . 9
⊢ (𝑦 ∈
Cℋ → (((⊥‘𝑦) ∈ Cℋ
→ (𝐵 ⊆
(⊥‘𝑦) →
(((⊥‘𝑦) ∩
𝐴) ∨ℋ
𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵)))) → (𝐵 ⊆ (⊥‘𝑦) → (((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))))) |
54 | 53 | adantl 485 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (((⊥‘𝑦) ∈ Cℋ
→ (𝐵 ⊆
(⊥‘𝑦) →
(((⊥‘𝑦) ∩
𝐴) ∨ℋ
𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵)))) → (𝐵 ⊆ (⊥‘𝑦) → (((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))))) |
55 | | chsscon2 29429 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
→ (𝐵 ⊆
(⊥‘𝑦) ↔
𝑦 ⊆
(⊥‘𝐵))) |
56 | 55 | biimprd 251 |
. . . . . . . . . 10
⊢ ((𝐵 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
→ (𝑦 ⊆
(⊥‘𝐵) →
𝐵 ⊆
(⊥‘𝑦))) |
57 | 56 | adantll 714 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (𝑦 ⊆ (⊥‘𝐵) → 𝐵 ⊆ (⊥‘𝑦))) |
58 | | fveq2 6668 |
. . . . . . . . . 10
⊢
((((⊥‘𝑦)
∩ 𝐴)
∨ℋ 𝐵) =
((⊥‘𝑦) ∩
(𝐴 ∨ℋ
𝐵)) →
(⊥‘(((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵)) = (⊥‘((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵)))) |
59 | | chincl 29426 |
. . . . . . . . . . . . . . . 16
⊢
(((⊥‘𝑦)
∈ Cℋ ∧ 𝐴 ∈ Cℋ )
→ ((⊥‘𝑦)
∩ 𝐴) ∈
Cℋ ) |
60 | 51, 59 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ ((⊥‘𝑦)
∩ 𝐴) ∈
Cℋ ) |
61 | | chdmj1 29456 |
. . . . . . . . . . . . . . 15
⊢
((((⊥‘𝑦)
∩ 𝐴) ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (⊥‘(((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵)) = ((⊥‘((⊥‘𝑦) ∩ 𝐴)) ∩ (⊥‘𝐵))) |
62 | 60, 61 | sylan 583 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
∧ 𝐵 ∈
Cℋ ) →
(⊥‘(((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵)) = ((⊥‘((⊥‘𝑦) ∩ 𝐴)) ∩ (⊥‘𝐵))) |
63 | | chdmm2 29453 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (⊥‘((⊥‘𝑦) ∩ 𝐴)) = (𝑦 ∨ℋ (⊥‘𝐴))) |
64 | 63 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
∧ 𝐵 ∈
Cℋ ) → (⊥‘((⊥‘𝑦) ∩ 𝐴)) = (𝑦 ∨ℋ (⊥‘𝐴))) |
65 | 64 | ineq1d 4100 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
∧ 𝐵 ∈
Cℋ ) →
((⊥‘((⊥‘𝑦) ∩ 𝐴)) ∩ (⊥‘𝐵)) = ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) |
66 | 62, 65 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
∧ 𝐵 ∈
Cℋ ) →
(⊥‘(((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵)) = ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) |
67 | 66 | anasss 470 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) →
(⊥‘(((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵)) = ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵))) |
68 | | chjcl 29284 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
∨ℋ 𝐵)
∈ Cℋ ) |
69 | | chdmm2 29453 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ )
→ (⊥‘((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))) = (𝑦 ∨ℋ (⊥‘(𝐴 ∨ℋ 𝐵)))) |
70 | 68, 69 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) →
(⊥‘((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))) = (𝑦 ∨ℋ (⊥‘(𝐴 ∨ℋ 𝐵)))) |
71 | | chdmj1 29456 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (⊥‘(𝐴
∨ℋ 𝐵))
= ((⊥‘𝐴) ∩
(⊥‘𝐵))) |
72 | 71 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) → (⊥‘(𝐴 ∨ℋ 𝐵)) = ((⊥‘𝐴) ∩ (⊥‘𝐵))) |
73 | 72 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) → (𝑦 ∨ℋ (⊥‘(𝐴 ∨ℋ 𝐵))) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵)))) |
74 | 70, 73 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) →
(⊥‘((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵)))) |
75 | 67, 74 | eqeq12d 2754 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈
Cℋ ∧ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ )) →
((⊥‘(((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵)) = (⊥‘((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))) ↔ ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵))))) |
76 | 75 | ancoms 462 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) →
((⊥‘(((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵)) = (⊥‘((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))) ↔ ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵))))) |
77 | 58, 76 | syl5ib 247 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → ((((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵)) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵))))) |
78 | 57, 77 | imim12d 81 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → ((𝐵 ⊆ (⊥‘𝑦) → (((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵))) → (𝑦 ⊆ (⊥‘𝐵) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵)))))) |
79 | 54, 78 | syld 47 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
∧ 𝑦 ∈
Cℋ ) → (((⊥‘𝑦) ∈ Cℋ
→ (𝐵 ⊆
(⊥‘𝑦) →
(((⊥‘𝑦) ∩
𝐴) ∨ℋ
𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵)))) → (𝑦 ⊆ (⊥‘𝐵) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵)))))) |
80 | 79 | ex 416 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑦 ∈
Cℋ → (((⊥‘𝑦) ∈ Cℋ
→ (𝐵 ⊆
(⊥‘𝑦) →
(((⊥‘𝑦) ∩
𝐴) ∨ℋ
𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵)))) → (𝑦 ⊆ (⊥‘𝐵) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵))))))) |
81 | 80 | com23 86 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (((⊥‘𝑦)
∈ Cℋ → (𝐵 ⊆ (⊥‘𝑦) → (((⊥‘𝑦) ∩ 𝐴) ∨ℋ 𝐵) = ((⊥‘𝑦) ∩ (𝐴 ∨ℋ 𝐵)))) → (𝑦 ∈ Cℋ
→ (𝑦 ⊆
(⊥‘𝐵) →
((𝑦 ∨ℋ
(⊥‘𝐴)) ∩
(⊥‘𝐵)) = (𝑦 ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵))))))) |
82 | 50, 81 | syl5 34 |
. . . 4
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑥 ∈
Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))) → (𝑦 ∈ Cℋ
→ (𝑦 ⊆
(⊥‘𝐵) →
((𝑦 ∨ℋ
(⊥‘𝐴)) ∩
(⊥‘𝐵)) = (𝑦 ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵))))))) |
83 | 82 | ralrimdv 3100 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑥 ∈
Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))) → ∀𝑦 ∈ Cℋ
(𝑦 ⊆
(⊥‘𝐵) →
((𝑦 ∨ℋ
(⊥‘𝐴)) ∩
(⊥‘𝐵)) = (𝑦 ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))) |
84 | 43, 83 | impbid 215 |
. 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ (⊥‘𝐵) → ((𝑦 ∨ℋ (⊥‘𝐴)) ∩ (⊥‘𝐵)) = (𝑦 ∨ℋ ((⊥‘𝐴) ∩ (⊥‘𝐵)))) ↔ ∀𝑥 ∈
Cℋ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) |
85 | | mdbr 30221 |
. . 3
⊢
(((⊥‘𝐴)
∈ Cℋ ∧ (⊥‘𝐵) ∈ Cℋ )
→ ((⊥‘𝐴)
𝑀ℋ (⊥‘𝐵) ↔ ∀𝑦 ∈ Cℋ
(𝑦 ⊆
(⊥‘𝐵) →
((𝑦 ∨ℋ
(⊥‘𝐴)) ∩
(⊥‘𝐵)) = (𝑦 ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))) |
86 | 16, 26, 85 | syl2an 599 |
. 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((⊥‘𝐴)
𝑀ℋ (⊥‘𝐵) ↔ ∀𝑦 ∈ Cℋ
(𝑦 ⊆
(⊥‘𝐵) →
((𝑦 ∨ℋ
(⊥‘𝐴)) ∩
(⊥‘𝐵)) = (𝑦 ∨ℋ
((⊥‘𝐴) ∩
(⊥‘𝐵)))))) |
87 | | dmdbr 30226 |
. 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ
(𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) |
88 | 84, 86, 87 | 3bitr4rd 315 |
1
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝐵 ↔ (⊥‘𝐴) 𝑀ℋ
(⊥‘𝐵))) |