| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mdexch.3 | . . . . . . . . . . . . . . 15
⊢ 𝐶 ∈
Cℋ | 
| 2 |  | mdexch.1 | . . . . . . . . . . . . . . 15
⊢ 𝐴 ∈
Cℋ | 
| 3 |  | chjass 31552 | . . . . . . . . . . . . . . 15
⊢ ((𝐶 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → ((𝐶 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐶 ∨ℋ (𝐴 ∨ℋ 𝑥))) | 
| 4 | 1, 2, 3 | mp3an12 1453 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → ((𝐶 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐶 ∨ℋ (𝐴 ∨ℋ 𝑥))) | 
| 5 | 1, 2 | chjcli 31476 | . . . . . . . . . . . . . . 15
⊢ (𝐶 ∨ℋ 𝐴) ∈
Cℋ | 
| 6 |  | chjcom 31525 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∨ℋ 𝐴) ∈ Cℋ )
→ (𝑥
∨ℋ (𝐶
∨ℋ 𝐴))
= ((𝐶
∨ℋ 𝐴)
∨ℋ 𝑥)) | 
| 7 | 5, 6 | mpan2 691 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) = ((𝐶 ∨ℋ 𝐴) ∨ℋ 𝑥)) | 
| 8 |  | chjcl 31376 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) | 
| 9 | 2, 8 | mpan 690 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → (𝐴 ∨ℋ 𝑥) ∈ Cℋ
) | 
| 10 |  | chjcom 31525 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∨ℋ 𝑥) ∈
Cℋ ∧ 𝐶 ∈ Cℋ )
→ ((𝐴
∨ℋ 𝑥)
∨ℋ 𝐶) =
(𝐶 ∨ℋ
(𝐴 ∨ℋ
𝑥))) | 
| 11 | 9, 1, 10 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) = (𝐶 ∨ℋ (𝐴 ∨ℋ 𝑥))) | 
| 12 | 4, 7, 11 | 3eqtr4d 2787 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶)) | 
| 13 | 12 | ineq1d 4219 | . . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ 𝐵)) | 
| 14 |  | inass 4228 | . . . . . . . . . . . . 13
⊢ ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) | 
| 15 |  | incom 4209 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) = (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) | 
| 16 |  | mdexch.2 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐵 ∈
Cℋ | 
| 17 | 2, 16 | chjcomi 31487 | . . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) | 
| 18 | 17 | ineq2i 4217 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = (𝐵 ∩ (𝐵 ∨ℋ 𝐴)) | 
| 19 | 16, 2 | chabs2i 31538 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 ∩ (𝐵 ∨ℋ 𝐴)) = 𝐵 | 
| 20 | 18, 19 | eqtri 2765 | . . . . . . . . . . . . . . 15
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐵 | 
| 21 | 15, 20 | eqtri 2765 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) = 𝐵 | 
| 22 | 21 | ineq2i 4217 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ 𝐵) | 
| 23 | 14, 22 | eqtri 2765 | . . . . . . . . . . . 12
⊢ ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ 𝐵) | 
| 24 | 13, 23 | eqtr4di 2795 | . . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) = ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵)) | 
| 25 | 24 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) = ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵)) | 
| 26 |  | chlej2 31530 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) ∧ 𝑥 ⊆ 𝐵) → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵)) | 
| 27 | 26 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) → (𝑥 ⊆ 𝐵 → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) | 
| 28 | 16, 2, 27 | mp3an23 1455 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) | 
| 29 | 2, 16 | chjcli 31476 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∨ℋ 𝐵) ∈
Cℋ | 
| 30 |  | mdi 32314 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵))) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) | 
| 31 | 30 | exp32 420 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ (𝐴
∨ℋ 𝑥)
∈ Cℋ ) → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) | 
| 32 | 1, 29, 31 | mp3an12 1453 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∨ℋ 𝑥) ∈
Cℋ → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) | 
| 33 | 9, 32 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) | 
| 34 | 33 | com23 86 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ⊆ (𝐴 ∨ℋ 𝐵) → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) | 
| 35 | 28, 34 | syld 47 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) | 
| 36 | 35 | imp31 417 | . . . . . . . . . . . . 13
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵)) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) | 
| 37 | 36 | adantrr 717 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) | 
| 38 | 1, 29 | chincli 31479 | . . . . . . . . . . . . . . . . 17
⊢ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∈
Cℋ | 
| 39 |  | chlej2 31530 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ )
∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴)) | 
| 40 | 39 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝑥) ∈ Cℋ )
→ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴))) | 
| 41 | 38, 2, 40 | mp3an12 1453 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∨ℋ 𝑥) ∈
Cℋ → ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴))) | 
| 42 | 9, 41 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴))) | 
| 43 | 42 | imp 406 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴)) | 
| 44 |  | chjcom 31525 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∨ℋ 𝑥) ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ ((𝐴
∨ℋ 𝑥)
∨ℋ 𝐴) =
(𝐴 ∨ℋ
(𝐴 ∨ℋ
𝑥))) | 
| 45 | 9, 2, 44 | sylancl 586 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴) = (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥))) | 
| 46 | 2 | chjidmi 31540 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∨ℋ 𝐴) = 𝐴 | 
| 47 | 46 | oveq1i 7441 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐴 ∨ℋ 𝑥) | 
| 48 |  | chjass 31552 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → ((𝐴 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥))) | 
| 49 | 2, 2, 48 | mp3an12 1453 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝐴) ∨ℋ 𝑥) = (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥))) | 
| 50 |  | chjcom 31525 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ (𝐴
∨ℋ 𝑥) =
(𝑥 ∨ℋ
𝐴)) | 
| 51 | 2, 50 | mpan 690 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
Cℋ → (𝐴 ∨ℋ 𝑥) = (𝑥 ∨ℋ 𝐴)) | 
| 52 | 47, 49, 51 | 3eqtr3a 2801 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → (𝐴 ∨ℋ (𝐴 ∨ℋ 𝑥)) = (𝑥 ∨ℋ 𝐴)) | 
| 53 | 45, 52 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴) = (𝑥 ∨ℋ 𝐴)) | 
| 54 | 53 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐴) = (𝑥 ∨ℋ 𝐴)) | 
| 55 | 43, 54 | sseqtrd 4020 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈
Cℋ ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ (𝑥 ∨ℋ 𝐴)) | 
| 56 | 55 | ad2ant2rl 749 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝐴 ∨ℋ 𝑥) ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) ⊆ (𝑥 ∨ℋ 𝐴)) | 
| 57 | 37, 56 | eqsstrd 4018 | . . . . . . . . . . 11
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → (((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ⊆ (𝑥 ∨ℋ 𝐴)) | 
| 58 | 57 | ssrind 4244 | . . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((((𝐴 ∨ℋ 𝑥) ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) | 
| 59 | 25, 58 | eqsstrd 4018 | . . . . . . . . 9
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) | 
| 60 | 59 | adantrl 716 | . . . . . . . 8
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴))) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ ((𝑥 ∨ℋ 𝐴) ∩ 𝐵)) | 
| 61 |  | mdi 32314 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝑥 ⊆ 𝐵)) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) | 
| 62 | 61 | exp32 420 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ
∧ 𝑥 ∈
Cℋ ) → (𝐴 𝑀ℋ 𝐵 → (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) | 
| 63 | 2, 16, 62 | mp3an12 1453 | . . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → (𝐴 𝑀ℋ 𝐵 → (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) | 
| 64 | 63 | com23 86 | . . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → (𝐴 𝑀ℋ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) | 
| 65 | 64 | imp31 417 | . . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐴 𝑀ℋ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) = (𝑥 ∨ℋ (𝐴 ∩ 𝐵))) | 
| 66 | 2, 1 | chub2i 31489 | . . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐶 ∨ℋ 𝐴) | 
| 67 |  | ssrin 4242 | . . . . . . . . . . . . 13
⊢ (𝐴 ⊆ (𝐶 ∨ℋ 𝐴) → (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)) | 
| 68 | 66, 67 | ax-mp 5 | . . . . . . . . . . . 12
⊢ (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) | 
| 69 | 2, 16 | chincli 31479 | . . . . . . . . . . . . 13
⊢ (𝐴 ∩ 𝐵) ∈
Cℋ | 
| 70 | 5, 16 | chincli 31479 | . . . . . . . . . . . . 13
⊢ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) ∈
Cℋ | 
| 71 |  | chlej2 31530 | . . . . . . . . . . . . . 14
⊢ ((((𝐴 ∩ 𝐵) ∈ Cℋ
∧ ((𝐶
∨ℋ 𝐴)
∩ 𝐵) ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
∧ (𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) | 
| 72 | 71 | ex 412 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∩ 𝐵) ∈ Cℋ
∧ ((𝐶
∨ℋ 𝐴)
∩ 𝐵) ∈
Cℋ ∧ 𝑥 ∈ Cℋ )
→ ((𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) | 
| 73 | 69, 70, 72 | mp3an12 1453 | . . . . . . . . . . . 12
⊢ (𝑥 ∈
Cℋ → ((𝐴 ∩ 𝐵) ⊆ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) | 
| 74 | 68, 73 | mpi 20 | . . . . . . . . . . 11
⊢ (𝑥 ∈
Cℋ → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) | 
| 75 | 74 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐴 𝑀ℋ 𝐵) → (𝑥 ∨ℋ (𝐴 ∩ 𝐵)) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) | 
| 76 | 65, 75 | eqsstrd 4018 | . . . . . . . . 9
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ 𝐴 𝑀ℋ 𝐵) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) | 
| 77 | 76 | adantrr 717 | . . . . . . . 8
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴))) → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) | 
| 78 | 60, 77 | sstrd 3994 | . . . . . . 7
⊢ (((𝑥 ∈
Cℋ ∧ 𝑥 ⊆ 𝐵) ∧ (𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴))) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))) | 
| 79 | 78 | exp31 419 | . . . . . 6
⊢ (𝑥 ∈
Cℋ → (𝑥 ⊆ 𝐵 → ((𝐴 𝑀ℋ 𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) | 
| 80 | 79 | com3r 87 | . . . . 5
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴)) → (𝑥 ∈ Cℋ
→ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) | 
| 81 | 80 | 3impb 1115 | . . . 4
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → (𝑥 ∈ Cℋ
→ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) | 
| 82 | 81 | ralrimiv 3145 | . . 3
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) | 
| 83 |  | mdbr2 32315 | . . . 4
⊢ (((𝐶 ∨ℋ 𝐴) ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ ((𝐶
∨ℋ 𝐴)
𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ
(𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵))))) | 
| 84 | 5, 16, 83 | mp2an 692 | . . 3
⊢ ((𝐶 ∨ℋ 𝐴) 𝑀ℋ
𝐵 ↔ ∀𝑥 ∈
Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ (𝐶 ∨ℋ 𝐴)) ∩ 𝐵) ⊆ (𝑥 ∨ℋ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵)))) | 
| 85 | 82, 84 | sylibr 234 | . 2
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → (𝐶 ∨ℋ 𝐴) 𝑀ℋ 𝐵) | 
| 86 | 1, 2 | chjcomi 31487 | . . . . 5
⊢ (𝐶 ∨ℋ 𝐴) = (𝐴 ∨ℋ 𝐶) | 
| 87 |  | incom 4209 | . . . . . 6
⊢ (𝐵 ∩ (𝐴 ∨ℋ 𝐵)) = ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) | 
| 88 | 18, 87, 19 | 3eqtr3ri 2774 | . . . . 5
⊢ 𝐵 = ((𝐴 ∨ℋ 𝐵) ∩ 𝐵) | 
| 89 | 86, 88 | ineq12i 4218 | . . . 4
⊢ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = ((𝐴 ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) | 
| 90 |  | inass 4228 | . . . . 5
⊢ (((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = ((𝐴 ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) | 
| 91 | 2, 16 | chub1i 31488 | . . . . . . . 8
⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵) | 
| 92 |  | mdi 32314 | . . . . . . . . . 10
⊢ (((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) ∧ (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵))) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) | 
| 93 | 92 | exp32 420 | . . . . . . . . 9
⊢ ((𝐶 ∈
Cℋ ∧ (𝐴 ∨ℋ 𝐵) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) → (𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) → (𝐴 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))))) | 
| 94 | 1, 29, 2, 93 | mp3an 1463 | . . . . . . . 8
⊢ (𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) → (𝐴 ⊆ (𝐴 ∨ℋ 𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))))) | 
| 95 | 91, 94 | mpi 20 | . . . . . . 7
⊢ (𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)))) | 
| 96 | 2, 38 | chjcomi 31487 | . . . . . . . 8
⊢ (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) = ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐴) | 
| 97 | 38, 2 | chlejb1i 31495 | . . . . . . . . 9
⊢ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 ↔ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐴) = 𝐴) | 
| 98 | 97 | biimpi 216 | . . . . . . . 8
⊢ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ∨ℋ 𝐴) = 𝐴) | 
| 99 | 96, 98 | eqtrid 2789 | . . . . . . 7
⊢ ((𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴 → (𝐴 ∨ℋ (𝐶 ∩ (𝐴 ∨ℋ 𝐵))) = 𝐴) | 
| 100 | 95, 99 | sylan9eq 2797 | . . . . . 6
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴) | 
| 101 | 100 | ineq1d 4219 | . . . . 5
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → (((𝐴 ∨ℋ 𝐶) ∩ (𝐴 ∨ℋ 𝐵)) ∩ 𝐵) = (𝐴 ∩ 𝐵)) | 
| 102 | 90, 101 | eqtr3id 2791 | . . . 4
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐴 ∨ℋ 𝐶) ∩ ((𝐴 ∨ℋ 𝐵) ∩ 𝐵)) = (𝐴 ∩ 𝐵)) | 
| 103 | 89, 102 | eqtrid 2789 | . . 3
⊢ ((𝐶 𝑀ℋ
(𝐴 ∨ℋ
𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵)) | 
| 104 | 103 | 3adant1 1131 | . 2
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵)) | 
| 105 | 85, 104 | jca 511 | 1
⊢ ((𝐴 𝑀ℋ
𝐵 ∧ 𝐶 𝑀ℋ (𝐴 ∨ℋ 𝐵) ∧ (𝐶 ∩ (𝐴 ∨ℋ 𝐵)) ⊆ 𝐴) → ((𝐶 ∨ℋ 𝐴) 𝑀ℋ 𝐵 ∧ ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐴 ∩ 𝐵))) |