| Step | Hyp | Ref
| Expression |
| 1 | | breq2 5147 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 𝑀ℋ 𝑥 ↔ 𝐴 𝑀ℋ 𝑦)) |
| 2 | 1 | cbvralvw 3237 |
. . . 4
⊢
(∀𝑥 ∈
Cℋ 𝐴 𝑀ℋ 𝑥 ↔ ∀𝑦 ∈
Cℋ 𝐴 𝑀ℋ 𝑦) |
| 3 | | mdbr 32313 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
→ (𝐴
𝑀ℋ 𝑦 ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑦 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑦) = (𝑥 ∨ℋ (𝐴 ∩ 𝑦))))) |
| 4 | | chjcom 31525 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐴
∨ℋ 𝑥) =
(𝑥 ∨ℋ
𝐴)) |
| 5 | 4 | ineq1d 4219 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ ((𝐴
∨ℋ 𝑥)
∩ 𝑦) = ((𝑥 ∨ℋ 𝐴) ∩ 𝑦)) |
| 6 | | incom 4209 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∨ℋ 𝑥) ∩ 𝑦) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥)) |
| 7 | 5, 6 | eqtr3di 2792 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ ((𝑥
∨ℋ 𝐴)
∩ 𝑦) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))) |
| 8 | 7 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → ((𝑥 ∨ℋ 𝐴) ∩ 𝑦) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))) |
| 9 | | chincl 31518 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
→ (𝐴 ∩ 𝑦) ∈
Cℋ ) |
| 10 | | chjcom 31525 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∩ 𝑦) ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → ((𝐴 ∩ 𝑦) ∨ℋ 𝑥) = (𝑥 ∨ℋ (𝐴 ∩ 𝑦))) |
| 11 | 9, 10 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → ((𝐴 ∩ 𝑦) ∨ℋ 𝑥) = (𝑥 ∨ℋ (𝐴 ∩ 𝑦))) |
| 12 | | incom 4209 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ 𝑦) = (𝑦 ∩ 𝐴) |
| 13 | 12 | oveq1i 7441 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝑦) ∨ℋ 𝑥) = ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) |
| 14 | 11, 13 | eqtr3di 2792 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → (𝑥 ∨ℋ (𝐴 ∩ 𝑦)) = ((𝑦 ∩ 𝐴) ∨ℋ 𝑥)) |
| 15 | 8, 14 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → (((𝑥 ∨ℋ 𝐴) ∩ 𝑦) = (𝑥 ∨ℋ (𝐴 ∩ 𝑦)) ↔ (𝑦 ∩ (𝐴 ∨ℋ 𝑥)) = ((𝑦 ∩ 𝐴) ∨ℋ 𝑥))) |
| 16 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝑦 ∩ (𝐴 ∨ℋ 𝑥)) = ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) ↔ ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))) |
| 17 | 15, 16 | bitrdi 287 |
. . . . . . . 8
⊢ (((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → (((𝑥 ∨ℋ 𝐴) ∩ 𝑦) = (𝑥 ∨ℋ (𝐴 ∩ 𝑦)) ↔ ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥)))) |
| 18 | 17 | imbi2d 340 |
. . . . . . 7
⊢ (((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
∧ 𝑥 ∈
Cℋ ) → ((𝑥 ⊆ 𝑦 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑦) = (𝑥 ∨ℋ (𝐴 ∩ 𝑦))) ↔ (𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))))) |
| 19 | 18 | ralbidva 3176 |
. . . . . 6
⊢ ((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
→ (∀𝑥 ∈
Cℋ (𝑥 ⊆ 𝑦 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑦) = (𝑥 ∨ℋ (𝐴 ∩ 𝑦))) ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))))) |
| 20 | 3, 19 | bitrd 279 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ 𝑦 ∈ Cℋ )
→ (𝐴
𝑀ℋ 𝑦 ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))))) |
| 21 | 20 | ralbidva 3176 |
. . . 4
⊢ (𝐴 ∈
Cℋ → (∀𝑦 ∈ Cℋ
𝐴
𝑀ℋ 𝑦 ↔ ∀𝑦 ∈ Cℋ
∀𝑥 ∈
Cℋ (𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))))) |
| 22 | 2, 21 | bitrid 283 |
. . 3
⊢ (𝐴 ∈
Cℋ → (∀𝑥 ∈ Cℋ
𝐴
𝑀ℋ 𝑥 ↔ ∀𝑦 ∈ Cℋ
∀𝑥 ∈
Cℋ (𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))))) |
| 23 | | ralcom 3289 |
. . 3
⊢
(∀𝑦 ∈
Cℋ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))) ↔ ∀𝑥 ∈ Cℋ
∀𝑦 ∈
Cℋ (𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥)))) |
| 24 | 22, 23 | bitrdi 287 |
. 2
⊢ (𝐴 ∈
Cℋ → (∀𝑥 ∈ Cℋ
𝐴
𝑀ℋ 𝑥 ↔ ∀𝑥 ∈ Cℋ
∀𝑦 ∈
Cℋ (𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))))) |
| 25 | | dmdbr 32318 |
. . 3
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝑥 ↔ ∀𝑦 ∈ Cℋ
(𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))))) |
| 26 | 25 | ralbidva 3176 |
. 2
⊢ (𝐴 ∈
Cℋ → (∀𝑥 ∈ Cℋ
𝐴
𝑀ℋ* 𝑥 ↔ ∀𝑥 ∈ Cℋ
∀𝑦 ∈
Cℋ (𝑥 ⊆ 𝑦 → ((𝑦 ∩ 𝐴) ∨ℋ 𝑥) = (𝑦 ∩ (𝐴 ∨ℋ 𝑥))))) |
| 27 | 24, 26 | bitr4d 282 |
1
⊢ (𝐴 ∈
Cℋ → (∀𝑥 ∈ Cℋ
𝐴
𝑀ℋ 𝑥 ↔ ∀𝑥 ∈ Cℋ
𝐴
𝑀ℋ* 𝑥)) |