| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | incom 4209 | . . . . . 6
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) | 
| 2 | 1 | sseq1i 4012 | . . . . 5
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ↔ (𝐵 ∩ 𝐴) ⊆ 𝑥) | 
| 3 | 2 | biimpri 228 | . . . 4
⊢ ((𝐵 ∩ 𝐴) ⊆ 𝑥 → (𝐴 ∩ 𝐵) ⊆ 𝑥) | 
| 4 |  | csmdsym.2 | . . . . . . . . . 10
⊢ 𝐵 ∈
Cℋ | 
| 5 |  | chjcom 31525 | . . . . . . . . . 10
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑥
∨ℋ 𝐵) =
(𝐵 ∨ℋ
𝑥)) | 
| 6 | 4, 5 | mpan2 691 | . . . . . . . . 9
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝑥)) | 
| 7 | 6 | ineq1d 4219 | . . . . . . . 8
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = ((𝐵 ∨ℋ 𝑥) ∩ 𝐴)) | 
| 8 |  | incom 4209 | . . . . . . . 8
⊢ ((𝐵 ∨ℋ 𝑥) ∩ 𝐴) = (𝐴 ∩ (𝐵 ∨ℋ 𝑥)) | 
| 9 | 7, 8 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = (𝐴 ∩ (𝐵 ∨ℋ 𝑥))) | 
| 10 | 9 | ad2antlr 727 | . . . . . 6
⊢
((((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = (𝐴 ∩ (𝐵 ∨ℋ 𝑥))) | 
| 11 | 4 | a1i 11 | . . . . . . . . 9
⊢ (𝑥 ∈
Cℋ → 𝐵 ∈ Cℋ
) | 
| 12 |  | id 22 | . . . . . . . . 9
⊢ (𝑥 ∈
Cℋ → 𝑥 ∈ Cℋ
) | 
| 13 |  | csmdsym.1 | . . . . . . . . . 10
⊢ 𝐴 ∈
Cℋ | 
| 14 | 13 | a1i 11 | . . . . . . . . 9
⊢ (𝑥 ∈
Cℋ → 𝐴 ∈ Cℋ
) | 
| 15 | 11, 12, 14 | 3jca 1129 | . . . . . . . 8
⊢ (𝑥 ∈
Cℋ → (𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
)) | 
| 16 | 15 | ad2antlr 727 | . . . . . . 7
⊢
((((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → (𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
)) | 
| 17 |  | inss2 4238 | . . . . . . . . . . . . 13
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 | 
| 18 |  | ssid 4006 | . . . . . . . . . . . . 13
⊢ 𝐵 ⊆ 𝐵 | 
| 19 | 17, 18 | pm3.2i 470 | . . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵) | 
| 20 |  | sseq2 4010 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
→ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ↔ (𝐴 ∩ 𝐵) ⊆ if(𝑥 ∈ Cℋ ,
𝑥,
0ℋ))) | 
| 21 |  | sseq1 4009 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
→ (𝑥 ⊆ 𝐴 ↔ if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
⊆ 𝐴)) | 
| 22 | 20, 21 | anbi12d 632 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
→ (((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) ↔ ((𝐴 ∩ 𝐵) ⊆ if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
∧ if(𝑥 ∈
Cℋ , 𝑥, 0ℋ) ⊆ 𝐴))) | 
| 23 | 22 | 3anbi2d 1443 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
→ ((𝐴
𝑀ℋ 𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) ↔ (𝐴 𝑀ℋ 𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
∧ if(𝑥 ∈
Cℋ , 𝑥, 0ℋ) ⊆ 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)))) | 
| 24 |  | breq1 5146 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
→ (𝑥
𝑀ℋ 𝐵 ↔ if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
𝑀ℋ 𝐵)) | 
| 25 | 23, 24 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑥 = if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
→ (((𝐴
𝑀ℋ 𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) → 𝑥 𝑀ℋ 𝐵) ↔ ((𝐴 𝑀ℋ 𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
∧ if(𝑥 ∈
Cℋ , 𝑥, 0ℋ) ⊆ 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) → if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
𝑀ℋ 𝐵))) | 
| 26 |  | h0elch 31274 | . . . . . . . . . . . . . . . 16
⊢
0ℋ ∈
Cℋ | 
| 27 | 26 | elimel 4595 | . . . . . . . . . . . . . . 15
⊢ if(𝑥 ∈
Cℋ , 𝑥, 0ℋ) ∈
Cℋ | 
| 28 | 13, 4, 27, 4 | mdslmd4i 32352 | . . . . . . . . . . . . . 14
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
∧ if(𝑥 ∈
Cℋ , 𝑥, 0ℋ) ⊆ 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) → if(𝑥 ∈ Cℋ ,
𝑥, 0ℋ)
𝑀ℋ 𝐵) | 
| 29 | 25, 28 | dedth 4584 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈
Cℋ → ((𝐴 𝑀ℋ 𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) → 𝑥 𝑀ℋ 𝐵)) | 
| 30 | 29 | com12 32 | . . . . . . . . . . . 12
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) → (𝑥 ∈ Cℋ
→ 𝑥
𝑀ℋ 𝐵)) | 
| 31 | 19, 30 | mp3an3 1452 | . . . . . . . . . . 11
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → (𝑥 ∈ Cℋ
→ 𝑥
𝑀ℋ 𝐵)) | 
| 32 | 31 | imp 406 | . . . . . . . . . 10
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) ∧ 𝑥 ∈ Cℋ )
→ 𝑥
𝑀ℋ 𝐵) | 
| 33 | 32 | an32s 652 | . . . . . . . . 9
⊢ (((𝐴 𝑀ℋ
𝐵 ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → 𝑥 𝑀ℋ 𝐵) | 
| 34 | 33 | adantlll 718 | . . . . . . . 8
⊢
((((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → 𝑥 𝑀ℋ 𝐵) | 
| 35 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝑥 → (𝑐 𝑀ℋ 𝐵 ↔ 𝑥 𝑀ℋ 𝐵)) | 
| 36 |  | breq2 5147 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝑥 → (𝐵 𝑀ℋ*
𝑐 ↔ 𝐵 𝑀ℋ*
𝑥)) | 
| 37 | 35, 36 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑐 = 𝑥 → ((𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ↔ (𝑥 𝑀ℋ
𝐵 → 𝐵 𝑀ℋ*
𝑥))) | 
| 38 | 37 | rspccva 3621 | . . . . . . . . . 10
⊢
((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝑥 ∈ Cℋ )
→ (𝑥
𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑥)) | 
| 39 | 38 | adantlr 715 | . . . . . . . . 9
⊢
(((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
→ (𝑥
𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑥)) | 
| 40 | 39 | adantr 480 | . . . . . . . 8
⊢
((((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → (𝑥 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑥)) | 
| 41 | 34, 40 | mpd 15 | . . . . . . 7
⊢
((((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → 𝐵 𝑀ℋ*
𝑥) | 
| 42 |  | simprr 773 | . . . . . . 7
⊢
((((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → 𝑥 ⊆ 𝐴) | 
| 43 |  | dmdi 32321 | . . . . . . 7
⊢ (((𝐵 ∈
Cℋ ∧ 𝑥 ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 𝑀ℋ*
𝑥 ∧ 𝑥 ⊆ 𝐴)) → ((𝐴 ∩ 𝐵) ∨ℋ 𝑥) = (𝐴 ∩ (𝐵 ∨ℋ 𝑥))) | 
| 44 | 16, 41, 42, 43 | syl12anc 837 | . . . . . 6
⊢
((((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → ((𝐴 ∩ 𝐵) ∨ℋ 𝑥) = (𝐴 ∩ (𝐵 ∨ℋ 𝑥))) | 
| 45 | 13, 4 | chincli 31479 | . . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ∈
Cℋ | 
| 46 |  | chjcom 31525 | . . . . . . . . 9
⊢ (((𝐴 ∩ 𝐵) ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → ((𝐴 ∩ 𝐵) ∨ℋ 𝑥) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) | 
| 47 | 45, 46 | mpan 690 | . . . . . . . 8
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∩ 𝐵) ∨ℋ 𝑥) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) | 
| 48 | 1 | oveq2i 7442 | . . . . . . . 8
⊢ (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) = (𝑥 ∨ℋ (𝐵 ∩ 𝐴)) | 
| 49 | 47, 48 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∩ 𝐵) ∨ℋ 𝑥) = (𝑥 ∨ℋ (𝐵 ∩ 𝐴))) | 
| 50 | 49 | ad2antlr 727 | . . . . . 6
⊢
((((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → ((𝐴 ∩ 𝐵) ∨ℋ 𝑥) = (𝑥 ∨ℋ (𝐵 ∩ 𝐴))) | 
| 51 | 10, 44, 50 | 3eqtr2d 2783 | . . . . 5
⊢
((((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
∧ ((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴)) → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = (𝑥 ∨ℋ (𝐵 ∩ 𝐴))) | 
| 52 | 51 | ex 412 | . . . 4
⊢
(((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
→ (((𝐴 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = (𝑥 ∨ℋ (𝐵 ∩ 𝐴)))) | 
| 53 | 3, 52 | sylani 604 | . . 3
⊢
(((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) ∧ 𝑥 ∈ Cℋ )
→ (((𝐵 ∩ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = (𝑥 ∨ℋ (𝐵 ∩ 𝐴)))) | 
| 54 | 53 | ralrimiva 3146 | . 2
⊢
((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) → ∀𝑥 ∈
Cℋ (((𝐵 ∩ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = (𝑥 ∨ℋ (𝐵 ∩ 𝐴)))) | 
| 55 | 4, 13 | mdsl2bi 32342 | . 2
⊢ (𝐵 𝑀ℋ
𝐴 ↔ ∀𝑥 ∈
Cℋ (((𝐵 ∩ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) → ((𝑥 ∨ℋ 𝐵) ∩ 𝐴) = (𝑥 ∨ℋ (𝐵 ∩ 𝐴)))) | 
| 56 | 54, 55 | sylibr 234 | 1
⊢
((∀𝑐 ∈
Cℋ (𝑐 𝑀ℋ 𝐵 → 𝐵 𝑀ℋ*
𝑐) ∧ 𝐴 𝑀ℋ 𝐵) → 𝐵 𝑀ℋ 𝐴) |