Proof of Theorem mdsymlem5
| Step | Hyp | Ref
| Expression |
| 1 | | df-ne 2941 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ≠ 𝑝 ↔ ¬ 𝑞 = 𝑝) |
| 2 | | atnemeq0 32396 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms) → (𝑞 ≠ 𝑝 ↔ (𝑞 ∩ 𝑝) = 0ℋ)) |
| 3 | 1, 2 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms) → (¬
𝑞 = 𝑝 ↔ (𝑞 ∩ 𝑝) = 0ℋ)) |
| 4 | 3 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms) → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ ¬ 𝑞 = 𝑝) ↔ (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ∩ 𝑝) = 0ℋ))) |
| 5 | 4 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ ¬ 𝑞 = 𝑝) ↔ (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ∩ 𝑝) = 0ℋ))) |
| 6 | | atelch 32363 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ HAtoms → 𝑞 ∈
Cℋ ) |
| 7 | | atexch 32400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑞 ∈
Cℋ ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ∩ 𝑝) = 0ℋ) → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝))) |
| 8 | 6, 7 | syl3an1 1164 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ∩ 𝑝) = 0ℋ) → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝))) |
| 9 | 5, 8 | sylbid 240 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ ¬ 𝑞 = 𝑝) → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝))) |
| 10 | 9 | expd 415 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ HAtoms ∧ 𝑝 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) → (¬ 𝑞 = 𝑝 → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝)))) |
| 11 | 10 | 3com23 1127 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) → (¬ 𝑞 = 𝑝 → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝)))) |
| 12 | 11 | 3expa 1119 |
. . . . . . . . . . . . . . 15
⊢ (((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) → (¬ 𝑞 = 𝑝 → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝)))) |
| 13 | 12 | adantrl 716 |
. . . . . . . . . . . . . 14
⊢ (((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) → (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) → (¬ 𝑞 = 𝑝 → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝)))) |
| 14 | 13 | adantrd 491 |
. . . . . . . . . . . . 13
⊢ (((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (¬ 𝑞 = 𝑝 → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝)))) |
| 15 | 14 | imp32 418 |
. . . . . . . . . . . 12
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝)) |
| 16 | 15 | adantrl 716 |
. . . . . . . . . . 11
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ (𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝))) → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝)) |
| 17 | 16 | adantrr 717 |
. . . . . . . . . 10
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ ((𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) ∧ 𝑝 ⊆ 𝑐)) → 𝑟 ⊆ (𝑞 ∨ℋ 𝑝)) |
| 18 | | simplrl 777 |
. . . . . . . . . . . 12
⊢ (((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝) → 𝑞 ⊆ 𝐴) |
| 19 | | atelch 32363 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ HAtoms → 𝑝 ∈
Cℋ ) |
| 20 | 19 | anim1i 615 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ HAtoms ∧ 𝑐 ∈
Cℋ ) → (𝑝 ∈ Cℋ
∧ 𝑐 ∈
Cℋ )) |
| 21 | 20 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms) → (𝑝 ∈ Cℋ
∧ 𝑐 ∈
Cℋ )) |
| 22 | | mdsymlem1.1 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐴 ∈
Cℋ |
| 23 | | chub2 31527 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈
Cℋ ∧ 𝑐 ∈ Cℋ )
→ 𝐴 ⊆ (𝑐 ∨ℋ 𝐴)) |
| 24 | 22, 23 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 ∈
Cℋ → 𝐴 ⊆ (𝑐 ∨ℋ 𝐴)) |
| 25 | | sstr 3992 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑞 ⊆ 𝐴 ∧ 𝐴 ⊆ (𝑐 ∨ℋ 𝐴)) → 𝑞 ⊆ (𝑐 ∨ℋ 𝐴)) |
| 26 | 24, 25 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑞 ⊆ 𝐴 ∧ 𝑐 ∈ Cℋ )
→ 𝑞 ⊆ (𝑐 ∨ℋ 𝐴)) |
| 27 | | chub1 31526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ 𝑐 ⊆ (𝑐 ∨ℋ 𝐴)) |
| 28 | 22, 27 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 ∈
Cℋ → 𝑐 ⊆ (𝑐 ∨ℋ 𝐴)) |
| 29 | | sstr 3992 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ⊆ 𝑐 ∧ 𝑐 ⊆ (𝑐 ∨ℋ 𝐴)) → 𝑝 ⊆ (𝑐 ∨ℋ 𝐴)) |
| 30 | 28, 29 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ⊆ 𝑐 ∧ 𝑐 ∈ Cℋ )
→ 𝑝 ⊆ (𝑐 ∨ℋ 𝐴)) |
| 31 | 26, 30 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑞 ⊆ 𝐴 ∧ 𝑐 ∈ Cℋ )
∧ (𝑝 ⊆ 𝑐 ∧ 𝑐 ∈ Cℋ ))
→ (𝑞 ⊆ (𝑐 ∨ℋ 𝐴) ∧ 𝑝 ⊆ (𝑐 ∨ℋ 𝐴))) |
| 32 | 31 | anandirs 679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐) ∧ 𝑐 ∈ Cℋ )
→ (𝑞 ⊆ (𝑐 ∨ℋ 𝐴) ∧ 𝑝 ⊆ (𝑐 ∨ℋ 𝐴))) |
| 33 | 32 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑐 ∈
Cℋ ∧ (𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐)) → (𝑞 ⊆ (𝑐 ∨ℋ 𝐴) ∧ 𝑝 ⊆ (𝑐 ∨ℋ 𝐴))) |
| 34 | 33 | adantll 714 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐)) → (𝑞 ⊆ (𝑐 ∨ℋ 𝐴) ∧ 𝑝 ⊆ (𝑐 ∨ℋ 𝐴))) |
| 35 | | chjcl 31376 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑐 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (𝑐
∨ℋ 𝐴)
∈ Cℋ ) |
| 36 | 22, 35 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 ∈
Cℋ → (𝑐 ∨ℋ 𝐴) ∈ Cℋ
) |
| 37 | | chlub 31528 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ
∧ (𝑐
∨ℋ 𝐴)
∈ Cℋ ) → ((𝑞 ⊆ (𝑐 ∨ℋ 𝐴) ∧ 𝑝 ⊆ (𝑐 ∨ℋ 𝐴)) ↔ (𝑞 ∨ℋ 𝑝) ⊆ (𝑐 ∨ℋ 𝐴))) |
| 38 | 36, 37 | syl3an3 1166 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ
∧ 𝑐 ∈
Cℋ ) → ((𝑞 ⊆ (𝑐 ∨ℋ 𝐴) ∧ 𝑝 ⊆ (𝑐 ∨ℋ 𝐴)) ↔ (𝑞 ∨ℋ 𝑝) ⊆ (𝑐 ∨ℋ 𝐴))) |
| 39 | 38 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) → ((𝑞 ⊆ (𝑐 ∨ℋ 𝐴) ∧ 𝑝 ⊆ (𝑐 ∨ℋ 𝐴)) ↔ (𝑞 ∨ℋ 𝑝) ⊆ (𝑐 ∨ℋ 𝐴))) |
| 40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐)) → ((𝑞 ⊆ (𝑐 ∨ℋ 𝐴) ∧ 𝑝 ⊆ (𝑐 ∨ℋ 𝐴)) ↔ (𝑞 ∨ℋ 𝑝) ⊆ (𝑐 ∨ℋ 𝐴))) |
| 41 | 34, 40 | mpbid 232 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐)) → (𝑞 ∨ℋ 𝑝) ⊆ (𝑐 ∨ℋ 𝐴)) |
| 42 | 41 | adantrl 716 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ (𝐴 ⊆ 𝑐 ∧ (𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐))) → (𝑞 ∨ℋ 𝑝) ⊆ (𝑐 ∨ℋ 𝐴)) |
| 43 | | chlejb2 31532 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈
Cℋ ∧ 𝑐 ∈ Cℋ )
→ (𝐴 ⊆ 𝑐 ↔ (𝑐 ∨ℋ 𝐴) = 𝑐)) |
| 44 | 22, 43 | mpan 690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∈
Cℋ → (𝐴 ⊆ 𝑐 ↔ (𝑐 ∨ℋ 𝐴) = 𝑐)) |
| 45 | 44 | biimpa 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) → (𝑐 ∨ℋ 𝐴) = 𝑐) |
| 46 | 45 | ad2ant2lr 748 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ (𝐴 ⊆ 𝑐 ∧ (𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐))) → (𝑐 ∨ℋ 𝐴) = 𝑐) |
| 47 | 42, 46 | sseqtrd 4020 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ (𝐴 ⊆ 𝑐 ∧ (𝑞 ⊆ 𝐴 ∧ 𝑝 ⊆ 𝑐))) → (𝑞 ∨ℋ 𝑝) ⊆ 𝑐) |
| 48 | 47 | exp45 438 |
. . . . . . . . . . . . . . 15
⊢ (((𝑞 ∈
Cℋ ∧ 𝑝 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) → (𝐴 ⊆ 𝑐 → (𝑞 ⊆ 𝐴 → (𝑝 ⊆ 𝑐 → (𝑞 ∨ℋ 𝑝) ⊆ 𝑐)))) |
| 49 | 48 | anasss 466 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ∈
Cℋ ∧ (𝑝 ∈ Cℋ
∧ 𝑐 ∈
Cℋ )) → (𝐴 ⊆ 𝑐 → (𝑞 ⊆ 𝐴 → (𝑝 ⊆ 𝑐 → (𝑞 ∨ℋ 𝑝) ⊆ 𝑐)))) |
| 50 | 6, 21, 49 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ HAtoms ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) → (𝐴 ⊆ 𝑐 → (𝑞 ⊆ 𝐴 → (𝑝 ⊆ 𝑐 → (𝑞 ∨ℋ 𝑝) ⊆ 𝑐)))) |
| 51 | 50 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) → (𝐴 ⊆ 𝑐 → (𝑞 ⊆ 𝐴 → (𝑝 ⊆ 𝑐 → (𝑞 ∨ℋ 𝑝) ⊆ 𝑐)))) |
| 52 | 18, 51 | syl7 74 |
. . . . . . . . . . 11
⊢ (((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) → (𝐴 ⊆ 𝑐 → (((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝) → (𝑝 ⊆ 𝑐 → (𝑞 ∨ℋ 𝑝) ⊆ 𝑐)))) |
| 53 | 52 | imp44 428 |
. . . . . . . . . 10
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ ((𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) ∧ 𝑝 ⊆ 𝑐)) → (𝑞 ∨ℋ 𝑝) ⊆ 𝑐) |
| 54 | 17, 53 | sstrd 3994 |
. . . . . . . . 9
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ ((𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) ∧ 𝑝 ⊆ 𝑐)) → 𝑟 ⊆ 𝑐) |
| 55 | | simplrr 778 |
. . . . . . . . . . 11
⊢ (((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝) → 𝑟 ⊆ 𝐵) |
| 56 | 55 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) ∧ 𝑝 ⊆ 𝑐) → 𝑟 ⊆ 𝐵) |
| 57 | 56 | adantl 481 |
. . . . . . . . 9
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ ((𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) ∧ 𝑝 ⊆ 𝑐)) → 𝑟 ⊆ 𝐵) |
| 58 | 54, 57 | ssind 4241 |
. . . . . . . 8
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ ((𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) ∧ 𝑝 ⊆ 𝑐)) → 𝑟 ⊆ (𝑐 ∩ 𝐵)) |
| 59 | | atelch 32363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ HAtoms → 𝑟 ∈
Cℋ ) |
| 60 | 6, 59 | anim12i 613 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ
)) |
| 61 | | mdsymlem1.2 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐵 ∈
Cℋ |
| 62 | | chincl 31518 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝑐 ∩ 𝐵) ∈
Cℋ ) |
| 63 | 61, 62 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 ∈
Cℋ → (𝑐 ∩ 𝐵) ∈ Cℋ
) |
| 64 | | chlej1 31529 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑟 ∈
Cℋ ∧ (𝑐 ∩ 𝐵) ∈ Cℋ
∧ 𝑞 ∈
Cℋ ) ∧ 𝑟 ⊆ (𝑐 ∩ 𝐵)) → (𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝑞)) |
| 65 | 64 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑟 ∈
Cℋ ∧ (𝑐 ∩ 𝐵) ∈ Cℋ
∧ 𝑞 ∈
Cℋ ) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → (𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝑞))) |
| 66 | 63, 65 | syl3an2 1165 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑟 ∈
Cℋ ∧ 𝑐 ∈ Cℋ
∧ 𝑞 ∈
Cℋ ) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → (𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝑞))) |
| 67 | 66 | 3comr 1126 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ
∧ 𝑐 ∈
Cℋ ) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → (𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝑞))) |
| 68 | 67 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → (𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝑞))) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ 𝑞 ⊆ 𝐴) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → (𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝑞))) |
| 70 | | chlej2 31530 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑞 ∈
Cℋ ∧ 𝐴 ∈ Cℋ
∧ (𝑐 ∩ 𝐵) ∈
Cℋ ) ∧ 𝑞 ⊆ 𝐴) → ((𝑐 ∩ 𝐵) ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)) |
| 71 | 22, 70 | mp3anl2 1458 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑞 ∈
Cℋ ∧ (𝑐 ∩ 𝐵) ∈ Cℋ )
∧ 𝑞 ⊆ 𝐴) → ((𝑐 ∩ 𝐵) ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)) |
| 72 | 63, 71 | sylanl2 681 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑞 ∈
Cℋ ∧ 𝑐 ∈ Cℋ )
∧ 𝑞 ⊆ 𝐴) → ((𝑐 ∩ 𝐵) ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)) |
| 73 | 72 | adantllr 719 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ 𝑞 ⊆ 𝐴) → ((𝑐 ∩ 𝐵) ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)) |
| 74 | | sstr2 3990 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝑞) → (((𝑐 ∩ 𝐵) ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) → (𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 75 | 73, 74 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ 𝑞 ⊆ 𝐴) → ((𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝑞) → (𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 76 | | chjcom 31525 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
→ (𝑞
∨ℋ 𝑟) =
(𝑟 ∨ℋ
𝑞)) |
| 77 | 76 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ 𝑞 ⊆ 𝐴) → (𝑞 ∨ℋ 𝑟) = (𝑟 ∨ℋ 𝑞)) |
| 78 | 77 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ 𝑞 ⊆ 𝐴) → ((𝑞 ∨ℋ 𝑟) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) ↔ (𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 79 | 75, 78 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ 𝑞 ⊆ 𝐴) → ((𝑟 ∨ℋ 𝑞) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝑞) → (𝑞 ∨ℋ 𝑟) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 80 | 69, 79 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ 𝑞 ⊆ 𝐴) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → (𝑞 ∨ℋ 𝑟) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 81 | 80 | adantrl 716 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ 𝑞 ⊆ 𝐴)) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → (𝑞 ∨ℋ 𝑟) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 82 | | sstr2 3990 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) → ((𝑞 ∨ℋ 𝑟) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 83 | 82 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ 𝑞 ⊆ 𝐴)) → ((𝑞 ∨ℋ 𝑟) ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 84 | 81, 83 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) ∧ (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ 𝑞 ⊆ 𝐴)) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 85 | 84 | exp32 420 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑞 ∈
Cℋ ∧ 𝑟 ∈ Cℋ )
∧ 𝑐 ∈
Cℋ ) → (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) → (𝑞 ⊆ 𝐴 → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))) |
| 86 | 60, 85 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ 𝑐 ∈
Cℋ ) → (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) → (𝑞 ⊆ 𝐴 → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))) |
| 87 | 86 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ (((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) → (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) → (𝑞 ⊆ 𝐴 → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))))) |
| 88 | 87 | imp31 417 |
. . . . . . . . . . . . 13
⊢
(((((𝑞 ∈ HAtoms
∧ 𝑟 ∈ HAtoms)
∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ 𝑝 ⊆ (𝑞 ∨ℋ 𝑟)) ∧ 𝑞 ⊆ 𝐴) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 89 | 88 | adantrr 717 |
. . . . . . . . . . . 12
⊢
(((((𝑞 ∈ HAtoms
∧ 𝑟 ∈ HAtoms)
∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ 𝑝 ⊆ (𝑞 ∨ℋ 𝑟)) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 90 | 89 | anasss 466 |
. . . . . . . . . . 11
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ (𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵))) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 91 | 90 | adantrr 717 |
. . . . . . . . . 10
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 92 | 91 | adantrl 716 |
. . . . . . . . 9
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ (𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝))) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 93 | 92 | adantrr 717 |
. . . . . . . 8
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ ((𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) ∧ 𝑝 ⊆ 𝑐)) → (𝑟 ⊆ (𝑐 ∩ 𝐵) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴))) |
| 94 | 58, 93 | mpd 15 |
. . . . . . 7
⊢ ((((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) ∧ ((𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) ∧ 𝑝 ⊆ 𝑐)) → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)) |
| 95 | 94 | exp32 420 |
. . . . . 6
⊢ (((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) → ((𝐴 ⊆ 𝑐 ∧ ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) ∧ ¬ 𝑞 = 𝑝)) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))) |
| 96 | 95 | exp4d 433 |
. . . . 5
⊢ (((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) ∧ (𝑐 ∈
Cℋ ∧ 𝑝 ∈ HAtoms)) → (𝐴 ⊆ 𝑐 → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (¬ 𝑞 = 𝑝 → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))))) |
| 97 | 96 | exp32 420 |
. . . 4
⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (𝑐 ∈
Cℋ → (𝑝 ∈ HAtoms → (𝐴 ⊆ 𝑐 → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (¬ 𝑞 = 𝑝 → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))))))) |
| 98 | 97 | com34 91 |
. . 3
⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (𝑐 ∈
Cℋ → (𝐴 ⊆ 𝑐 → (𝑝 ∈ HAtoms → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (¬ 𝑞 = 𝑝 → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))))))) |
| 99 | 98 | imp4c 423 |
. 2
⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (((𝑐 ∈
Cℋ ∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (¬ 𝑞 = 𝑝 → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))))) |
| 100 | 99 | com24 95 |
1
⊢ ((𝑞 ∈ HAtoms ∧ 𝑟 ∈ HAtoms) → (¬
𝑞 = 𝑝 → ((𝑝 ⊆ (𝑞 ∨ℋ 𝑟) ∧ (𝑞 ⊆ 𝐴 ∧ 𝑟 ⊆ 𝐵)) → (((𝑐 ∈ Cℋ
∧ 𝐴 ⊆ 𝑐) ∧ 𝑝 ∈ HAtoms) → (𝑝 ⊆ 𝑐 → 𝑝 ⊆ ((𝑐 ∩ 𝐵) ∨ℋ 𝐴)))))) |