| Step | Hyp | Ref
| Expression |
| 1 | | eleq1 2829 |
. . . . 5
⊢ (𝑦 = 𝐴 → (𝑦 ∈ Cℋ
↔ 𝐴 ∈
Cℋ )) |
| 2 | 1 | anbi1d 631 |
. . . 4
⊢ (𝑦 = 𝐴 → ((𝑦 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ↔ (𝐴 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ))) |
| 3 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑥 ∨ℋ 𝑦) = (𝑥 ∨ℋ 𝐴)) |
| 4 | 3 | ineq1d 4219 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ((𝑥 ∨ℋ 𝑦) ∩ 𝑧) = ((𝑥 ∨ℋ 𝐴) ∩ 𝑧)) |
| 5 | | ineq1 4213 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑦 ∩ 𝑧) = (𝐴 ∩ 𝑧)) |
| 6 | 5 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑥 ∨ℋ (𝑦 ∩ 𝑧)) = (𝑥 ∨ℋ (𝐴 ∩ 𝑧))) |
| 7 | 4, 6 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (((𝑥 ∨ℋ 𝑦) ∩ 𝑧) = (𝑥 ∨ℋ (𝑦 ∩ 𝑧)) ↔ ((𝑥 ∨ℋ 𝐴) ∩ 𝑧) = (𝑥 ∨ℋ (𝐴 ∩ 𝑧)))) |
| 8 | 7 | imbi2d 340 |
. . . . 5
⊢ (𝑦 = 𝐴 → ((𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝑦) ∩ 𝑧) = (𝑥 ∨ℋ (𝑦 ∩ 𝑧))) ↔ (𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑧) = (𝑥 ∨ℋ (𝐴 ∩ 𝑧))))) |
| 9 | 8 | ralbidv 3178 |
. . . 4
⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝑦) ∩ 𝑧) = (𝑥 ∨ℋ (𝑦 ∩ 𝑧))) ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑧) = (𝑥 ∨ℋ (𝐴 ∩ 𝑧))))) |
| 10 | 2, 9 | anbi12d 632 |
. . 3
⊢ (𝑦 = 𝐴 → (((𝑦 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝑦) ∩ 𝑧) = (𝑥 ∨ℋ (𝑦 ∩ 𝑧)))) ↔ ((𝐴 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑧) = (𝑥 ∨ℋ (𝐴 ∩ 𝑧)))))) |
| 11 | | eleq1 2829 |
. . . . 5
⊢ (𝑧 = 𝐵 → (𝑧 ∈ Cℋ
↔ 𝐵 ∈
Cℋ )) |
| 12 | 11 | anbi2d 630 |
. . . 4
⊢ (𝑧 = 𝐵 → ((𝐴 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ↔ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ ))) |
| 13 | | sseq2 4010 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (𝑥 ⊆ 𝑧 ↔ 𝑥 ⊆ 𝐵)) |
| 14 | | ineq2 4214 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑧) = ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) |
| 15 | | ineq2 4214 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝐴 ∩ 𝑧) = (𝐴 ∩ 𝐵)) |
| 16 | 15 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → (𝑥 ∨ℋ (𝐴 ∩ 𝑧)) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) |
| 17 | 14, 16 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (((𝑥 ∨ℋ 𝐴) ∩ 𝑧) = (𝑥 ∨ℋ (𝐴 ∩ 𝑧)) ↔ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))) |
| 18 | 13, 17 | imbi12d 344 |
. . . . 5
⊢ (𝑧 = 𝐵 → ((𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑧) = (𝑥 ∨ℋ (𝐴 ∩ 𝑧))) ↔ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |
| 19 | 18 | ralbidv 3178 |
. . . 4
⊢ (𝑧 = 𝐵 → (∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑧) = (𝑥 ∨ℋ (𝐴 ∩ 𝑧))) ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |
| 20 | 12, 19 | anbi12d 632 |
. . 3
⊢ (𝑧 = 𝐵 → (((𝐴 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝐴) ∩ 𝑧) = (𝑥 ∨ℋ (𝐴 ∩ 𝑧)))) ↔ ((𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))))) |
| 21 | | df-md 32299 |
. . 3
⊢
𝑀ℋ = {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝑧 → ((𝑥 ∨ℋ 𝑦) ∩ 𝑧) = (𝑥 ∨ℋ (𝑦 ∩ 𝑧))))} |
| 22 | 10, 20, 21 | brabg 5544 |
. 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ 𝐵 ↔ ((𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵)))))) |
| 23 | 22 | bianabs 541 |
1
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |