| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq1 2828 | . . . . 5
⊢ (𝑦 = 𝐴 → (𝑦 ∈ Cℋ
↔ 𝐴 ∈
Cℋ )) | 
| 2 | 1 | anbi1d 631 | . . . 4
⊢ (𝑦 = 𝐴 → ((𝑦 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ↔ (𝐴 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ))) | 
| 3 |  | ineq2 4213 | . . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑥 ∩ 𝑦) = (𝑥 ∩ 𝐴)) | 
| 4 | 3 | oveq1d 7447 | . . . . . . 7
⊢ (𝑦 = 𝐴 → ((𝑥 ∩ 𝑦) ∨ℋ 𝑧) = ((𝑥 ∩ 𝐴) ∨ℋ 𝑧)) | 
| 5 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑦 ∨ℋ 𝑧) = (𝐴 ∨ℋ 𝑧)) | 
| 6 | 5 | ineq2d 4219 | . . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑥 ∩ (𝑦 ∨ℋ 𝑧)) = (𝑥 ∩ (𝐴 ∨ℋ 𝑧))) | 
| 7 | 4, 6 | eqeq12d 2752 | . . . . . 6
⊢ (𝑦 = 𝐴 → (((𝑥 ∩ 𝑦) ∨ℋ 𝑧) = (𝑥 ∩ (𝑦 ∨ℋ 𝑧)) ↔ ((𝑥 ∩ 𝐴) ∨ℋ 𝑧) = (𝑥 ∩ (𝐴 ∨ℋ 𝑧)))) | 
| 8 | 7 | imbi2d 340 | . . . . 5
⊢ (𝑦 = 𝐴 → ((𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝑦) ∨ℋ 𝑧) = (𝑥 ∩ (𝑦 ∨ℋ 𝑧))) ↔ (𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝑧) = (𝑥 ∩ (𝐴 ∨ℋ 𝑧))))) | 
| 9 | 8 | ralbidv 3177 | . . . 4
⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ Cℋ
(𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝑦) ∨ℋ 𝑧) = (𝑥 ∩ (𝑦 ∨ℋ 𝑧))) ↔ ∀𝑥 ∈ Cℋ
(𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝑧) = (𝑥 ∩ (𝐴 ∨ℋ 𝑧))))) | 
| 10 | 2, 9 | anbi12d 632 | . . 3
⊢ (𝑦 = 𝐴 → (((𝑦 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝑦) ∨ℋ 𝑧) = (𝑥 ∩ (𝑦 ∨ℋ 𝑧)))) ↔ ((𝐴 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝑧) = (𝑥 ∩ (𝐴 ∨ℋ 𝑧)))))) | 
| 11 |  | eleq1 2828 | . . . . 5
⊢ (𝑧 = 𝐵 → (𝑧 ∈ Cℋ
↔ 𝐵 ∈
Cℋ )) | 
| 12 | 11 | anbi2d 630 | . . . 4
⊢ (𝑧 = 𝐵 → ((𝐴 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ↔ (𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ ))) | 
| 13 |  | sseq1 4008 | . . . . . 6
⊢ (𝑧 = 𝐵 → (𝑧 ⊆ 𝑥 ↔ 𝐵 ⊆ 𝑥)) | 
| 14 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑧 = 𝐵 → ((𝑥 ∩ 𝐴) ∨ℋ 𝑧) = ((𝑥 ∩ 𝐴) ∨ℋ 𝐵)) | 
| 15 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝐴 ∨ℋ 𝑧) = (𝐴 ∨ℋ 𝐵)) | 
| 16 | 15 | ineq2d 4219 | . . . . . . 7
⊢ (𝑧 = 𝐵 → (𝑥 ∩ (𝐴 ∨ℋ 𝑧)) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))) | 
| 17 | 14, 16 | eqeq12d 2752 | . . . . . 6
⊢ (𝑧 = 𝐵 → (((𝑥 ∩ 𝐴) ∨ℋ 𝑧) = (𝑥 ∩ (𝐴 ∨ℋ 𝑧)) ↔ ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))) | 
| 18 | 13, 17 | imbi12d 344 | . . . . 5
⊢ (𝑧 = 𝐵 → ((𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝑧) = (𝑥 ∩ (𝐴 ∨ℋ 𝑧))) ↔ (𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) | 
| 19 | 18 | ralbidv 3177 | . . . 4
⊢ (𝑧 = 𝐵 → (∀𝑥 ∈ Cℋ
(𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝑧) = (𝑥 ∩ (𝐴 ∨ℋ 𝑧))) ↔ ∀𝑥 ∈ Cℋ
(𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) | 
| 20 | 12, 19 | anbi12d 632 | . . 3
⊢ (𝑧 = 𝐵 → (((𝐴 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝑧) = (𝑥 ∩ (𝐴 ∨ℋ 𝑧)))) ↔ ((𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))))) | 
| 21 |  | df-dmd 32301 | . . 3
⊢ 
𝑀ℋ* = {〈𝑦, 𝑧〉 ∣ ((𝑦 ∈ Cℋ
∧ 𝑧 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝑧 ⊆ 𝑥 → ((𝑥 ∩ 𝑦) ∨ℋ 𝑧) = (𝑥 ∩ (𝑦 ∨ℋ 𝑧))))} | 
| 22 | 10, 20, 21 | brabg 5543 | . 2
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝐵 ↔ ((𝐴 ∈ Cℋ
∧ 𝐵 ∈
Cℋ ) ∧ ∀𝑥 ∈ Cℋ
(𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵)))))) | 
| 23 | 22 | bianabs 541 | 1
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
𝑀ℋ* 𝐵 ↔ ∀𝑥 ∈ Cℋ
(𝐵 ⊆ 𝑥 → ((𝑥 ∩ 𝐴) ∨ℋ 𝐵) = (𝑥 ∩ (𝐴 ∨ℋ 𝐵))))) |