Step | Hyp | Ref
| Expression |
1 | | mdbr 30656 |
. 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ 𝐵 ↔ ∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))))) |
2 | | chincl 29861 |
. . . . . . . 8
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑥 ∩ 𝐵) ∈
Cℋ ) |
3 | | inss2 4163 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝐵) ⊆ 𝐵 |
4 | | sseq1 3946 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑥 ∩ 𝐵) → (𝑦 ⊆ 𝐵 ↔ (𝑥 ∩ 𝐵) ⊆ 𝐵)) |
5 | | oveq1 7282 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑥 ∩ 𝐵) → (𝑦 ∨ℋ 𝐴) = ((𝑥 ∩ 𝐵) ∨ℋ 𝐴)) |
6 | 5 | ineq1d 4145 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 ∩ 𝐵) → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵)) |
7 | | oveq1 7282 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 ∩ 𝐵) → (𝑦 ∨ℋ (𝐴 ∩ 𝐵)) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵))) |
8 | 6, 7 | eqeq12d 2754 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑥 ∩ 𝐵) → (((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵)) ↔ (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) |
9 | 4, 8 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑥 ∩ 𝐵) → ((𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) ↔ ((𝑥 ∩ 𝐵) ⊆ 𝐵 → (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵))))) |
10 | 9 | rspcv 3557 |
. . . . . . . . 9
⊢ ((𝑥 ∩ 𝐵) ∈ Cℋ
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) → ((𝑥 ∩ 𝐵) ⊆ 𝐵 → (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵))))) |
11 | 3, 10 | mpii 46 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝐵) ∈ Cℋ
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) → (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) |
12 | 2, 11 | syl 17 |
. . . . . . 7
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) → (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) |
13 | 12 | ex 413 |
. . . . . 6
⊢ (𝑥 ∈
Cℋ → (𝐵 ∈ Cℋ
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) → (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵))))) |
14 | 13 | com3l 89 |
. . . . 5
⊢ (𝐵 ∈
Cℋ → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) → (𝑥 ∈ Cℋ
→ (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵))))) |
15 | 14 | ralrimdv 3105 |
. . . 4
⊢ (𝐵 ∈
Cℋ → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) → ∀𝑥 ∈ Cℋ
(((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) |
16 | | dfss 3905 |
. . . . . . . . . . 11
⊢ (𝑥 ⊆ 𝐵 ↔ 𝑥 = (𝑥 ∩ 𝐵)) |
17 | 16 | biimpi 215 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝐵 → 𝑥 = (𝑥 ∩ 𝐵)) |
18 | 17 | oveq1d 7290 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝐵 → (𝑥 ∨ℋ 𝐴) = ((𝑥 ∩ 𝐵) ∨ℋ 𝐴)) |
19 | 18 | ineq1d 4145 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵)) |
20 | 17 | oveq1d 7290 |
. . . . . . . 8
⊢ (𝑥 ⊆ 𝐵 → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵))) |
21 | 19, 20 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 ⊆ 𝐵 → (((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ↔ (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) |
22 | 21 | biimprcd 249 |
. . . . . 6
⊢ ((((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)) → (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))) |
23 | 22 | ralimi 3087 |
. . . . 5
⊢
(∀𝑥 ∈
Cℋ (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)) → ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))) |
24 | | sseq1 3946 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝐵 ↔ 𝑦 ⊆ 𝐵)) |
25 | | oveq1 7282 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ∨ℋ 𝐴) = (𝑦 ∨ℋ 𝐴)) |
26 | 25 | ineq1d 4145 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = ((𝑦 ∨ℋ 𝐴) ∩ 𝐵)) |
27 | | oveq1 7282 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) |
28 | 26, 27 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ↔ ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵)))) |
29 | 24, 28 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) ↔ (𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))))) |
30 | 29 | cbvralvw 3383 |
. . . . 5
⊢
(∀𝑥 ∈
Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) ↔ ∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵)))) |
31 | 23, 30 | sylib 217 |
. . . 4
⊢
(∀𝑥 ∈
Cℋ (((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)) → ∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵)))) |
32 | 15, 31 | impbid1 224 |
. . 3
⊢ (𝐵 ∈
Cℋ → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) ↔ ∀𝑥 ∈ Cℋ
(((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) |
33 | 32 | adantl 482 |
. 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐵 → ((𝑦 ∨ℋ 𝐴) ∩ 𝐵) = (𝑦 ∨ℋ (𝐴 ∩ 𝐵))) ↔ ∀𝑥 ∈ Cℋ
(((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) |
34 | 1, 33 | bitrd 278 |
1
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ
(((𝑥 ∩ 𝐵) ∨ℋ 𝐴) ∩ 𝐵) = ((𝑥 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐵)))) |