| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mdsymlem1.1 | . . . . . . . . . . . . 13
⊢ 𝐴 ∈
Cℋ | 
| 2 |  | mdsymlem1.2 | . . . . . . . . . . . . 13
⊢ 𝐵 ∈
Cℋ | 
| 3 | 1, 2 | chjcomi 31487 | . . . . . . . . . . . 12
⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) | 
| 4 | 3 | sseq2i 4013 | . . . . . . . . . . 11
⊢ (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) ↔ 𝑝 ⊆ (𝐵 ∨ℋ 𝐴)) | 
| 5 | 4 | anbi2i 623 | . . . . . . . . . 10
⊢ ((𝑝 ⊆ 𝑐 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ (𝑝 ⊆ 𝑐 ∧ 𝑝 ⊆ (𝐵 ∨ℋ 𝐴))) | 
| 6 |  | ssin 4239 | . . . . . . . . . 10
⊢ ((𝑝 ⊆ 𝑐 ∧ 𝑝 ⊆ (𝐵 ∨ℋ 𝐴)) ↔ 𝑝 ⊆ (𝑐 ∩ (𝐵 ∨ℋ 𝐴))) | 
| 7 | 5, 6 | bitri 275 | . . . . . . . . 9
⊢ ((𝑝 ⊆ 𝑐 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵)) ↔ 𝑝 ⊆ (𝑐 ∩ (𝐵 ∨ℋ 𝐴))) | 
| 8 |  | mdsymlem1.3 | . . . . . . . . . . . . . . . 16
⊢ 𝐶 = (𝐴 ∨ℋ 𝑝) | 
| 9 | 1, 2, 8 | mdsymlem5 32426 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (¬
𝑞 = 𝑝 → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (((𝑐 ∈ Cℋ
∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))))) | 
| 10 |  | sseq1 4009 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑞 = 𝑝 → (𝑞 ⊆ 𝐴 ↔ 𝑝 ⊆ 𝐴)) | 
| 11 |  | chincl 31518 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑐 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑐 ∩ 𝐵) ∈
Cℋ ) | 
| 12 | 2, 11 | mpan2 691 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 ∈
Cℋ → (𝑐 ∩ 𝐵) ∈ Cℋ
) | 
| 13 |  | chub2 31527 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈
Cℋ ∧ (𝑐 ∩ 𝐵) ∈ Cℋ )
→ 𝐴 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)) | 
| 14 | 1, 12, 13 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 ∈
Cℋ → 𝐴 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)) | 
| 15 |  | sstr2 3990 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑝 ⊆ 𝐴 → (𝐴 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) | 
| 16 | 14, 15 | syl5 34 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑝 ⊆ 𝐴 → (𝑐 ∈ Cℋ
→ 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) | 
| 17 | 10, 16 | biimtrdi 253 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 = 𝑝 → (𝑞 ⊆ 𝐴 → (𝑐 ∈ Cℋ
→ 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 18 | 17 | impd 410 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 = 𝑝 → ((𝑞 ⊆ 𝐴 ∧ 𝑐 ∈ Cℋ )
→ 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) | 
| 19 | 18 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ⊆ 𝑐 → (𝑞 = 𝑝 → ((𝑞 ⊆ 𝐴 ∧ 𝑐 ∈ Cℋ )
→ 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 20 | 19 | com13 88 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑞 ⊆ 𝐴 ∧ 𝑐 ∈ Cℋ )
→ (𝑞 = 𝑝 → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 21 | 20 | adantrr 717 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑞 ⊆ 𝐴 ∧ (𝑐 ∈ Cℋ
∧ 𝐴 ⊆ 𝑐)) → (𝑞 = 𝑝 → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 22 | 21 | ad2ant2r 747 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵) ∧ ((𝑐 ∈ Cℋ
∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms)) → (𝑞 = 𝑝 → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 23 | 22 | adantll 714 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ((𝑐 ∈ Cℋ
∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms)) → (𝑞 = 𝑝 → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 24 | 23 | com12 32 | . . . . . . . . . . . . . . . 16
⊢ (𝑞 = 𝑝 → (((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ((𝑐 ∈ Cℋ
∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms)) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 25 | 24 | expd 415 | . . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑝 → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (((𝑐 ∈ Cℋ
∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))) | 
| 26 | 9, 25 | pm2.61d2 181 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (((𝑐 ∈ Cℋ
∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))) | 
| 27 | 26 | rexlimivv 3201 | . . . . . . . . . . . . 13
⊢
(∃𝑞 ∈
HAtoms ∃𝑟 ∈
HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (((𝑐 ∈ Cℋ
∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 28 | 27 | com12 32 | . . . . . . . . . . . 12
⊢ (((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 29 | 28 | imim2d 57 | . . . . . . . . . . 11
⊢ (((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → ((𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))) | 
| 30 | 29 | com34 91 | . . . . . . . . . 10
⊢ (((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → ((𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → (𝑝 ⊆ 𝑐 → (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))) | 
| 31 | 30 | imp4b 421 | . . . . . . . . 9
⊢ ((((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) ∧ (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)))) → ((𝑝 ⊆ 𝑐 ∧ 𝑝 ⊆ (𝐴 ∨ℋ 𝐵)) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) | 
| 32 | 7, 31 | biimtrrid 243 | . . . . . . . 8
⊢ ((((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) ∧ (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)))) → (𝑝 ⊆ (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) | 
| 33 | 32 | ex 412 | . . . . . . 7
⊢ (((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → ((𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → (𝑝 ⊆ (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 34 | 33 | ralimdva 3167 | . . . . . 6
⊢ ((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) → (∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → ∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 35 | 2, 1 | chjcli 31476 | . . . . . . . . 9
⊢ (𝐵 ∨ℋ 𝐴) ∈
Cℋ | 
| 36 |  | chincl 31518 | . . . . . . . . 9
⊢ ((𝑐 ∈
Cℋ ∧ (𝐵 ∨ℋ 𝐴) ∈ Cℋ )
→ (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ∈
Cℋ ) | 
| 37 | 35, 36 | mpan2 691 | . . . . . . . 8
⊢ (𝑐 ∈
Cℋ → (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ∈ Cℋ
) | 
| 38 |  | chjcl 31376 | . . . . . . . . 9
⊢ (((𝑐 ∩ 𝐵) ∈ Cℋ
∧ 𝐴 ∈
Cℋ ) → ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) ∈ Cℋ
) | 
| 39 | 12, 1, 38 | sylancl 586 | . . . . . . . 8
⊢ (𝑐 ∈
Cℋ → ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) ∈ Cℋ
) | 
| 40 |  | chrelat3 32390 | . . . . . . . 8
⊢ (((𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ∈ Cℋ
∧ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) ∈
Cℋ ) → ((𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) ↔ ∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 41 | 37, 39, 40 | syl2anc 584 | . . . . . . 7
⊢ (𝑐 ∈
Cℋ → ((𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) ↔ ∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 42 | 41 | adantr 480 | . . . . . 6
⊢ ((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) → ((𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) ↔ ∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 43 | 34, 42 | sylibrd 259 | . . . . 5
⊢ ((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) → (∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) | 
| 44 | 43 | ex 412 | . . . 4
⊢ (𝑐 ∈
Cℋ → (𝐴 ⊆ 𝑐 → (∀𝑝 ∈ HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 45 | 44 | com3r 87 | . . 3
⊢
(∀𝑝 ∈
HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → (𝑐 ∈ Cℋ
→ (𝐴 ⊆ 𝑐 → (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 46 | 45 | ralrimiv 3145 | . 2
⊢
(∀𝑝 ∈
HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → ∀𝑐 ∈ Cℋ
(𝐴 ⊆ 𝑐 → (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) | 
| 47 |  | dmdbr2 32322 | . . 3
⊢ ((𝐵 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (𝐵
𝑀ℋ* 𝐴 ↔ ∀𝑐 ∈ Cℋ
(𝐴 ⊆ 𝑐 → (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) | 
| 48 | 2, 1, 47 | mp2an 692 | . 2
⊢ (𝐵
𝑀ℋ* 𝐴 ↔ ∀𝑐 ∈ Cℋ
(𝐴 ⊆ 𝑐 → (𝑐 ∩ (𝐵 ∨ℋ 𝐴)) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) | 
| 49 | 46, 48 | sylibr 234 | 1
⊢
(∀𝑝 ∈
HAtoms (𝑝 ⊆ (𝐴 ∨ℋ 𝐵) → ∃𝑞 ∈ HAtoms ∃𝑟 ∈ HAtoms (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → 𝐵 𝑀ℋ*
𝐴) |