Proof of Theorem chirredlem3
| Step | Hyp | Ref
| Expression |
| 1 | | atelch 32363 |
. . 3
⊢ (𝑞 ∈ HAtoms → 𝑞 ∈
Cℋ ) |
| 2 | | chirred.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈
Cℋ |
| 3 | 2 | chirredlem2 32410 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞)) = 𝑞) |
| 4 | 3 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑟 ∨ℋ 𝑞)) |
| 5 | | atelch 32363 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ HAtoms → 𝑟 ∈
Cℋ ) |
| 6 | 5 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → 𝑟 ∈ Cℋ
) |
| 7 | | atelch 32363 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ HAtoms → 𝑝 ∈
Cℋ ) |
| 8 | | chjcl 31376 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝑝
∨ℋ 𝑞)
∈ Cℋ ) |
| 9 | 7, 8 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈
Cℋ ) → (𝑝 ∨ℋ 𝑞) ∈ Cℋ
) |
| 10 | 9 | ad2ant2r 747 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) →
(𝑝 ∨ℋ
𝑞) ∈
Cℋ ) |
| 11 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) |
| 12 | | pjoml2 31630 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈
Cℋ ∧ (𝑝 ∨ℋ 𝑞) ∈ Cℋ
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞)) |
| 13 | 6, 10, 11, 12 | syl3an 1161 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ ((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞)) |
| 14 | 13 | 3com12 1124 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
(𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞)) |
| 15 | 14 | 3expb 1121 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞)) |
| 16 | 4, 15 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ 𝑞) = (𝑝 ∨ℋ 𝑞)) |
| 17 | 16 | ineq2d 4220 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = (𝐴 ∩ (𝑝 ∨ℋ 𝑞))) |
| 18 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑟 → (𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑟)) |
| 19 | | chirred.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → 𝐴 𝐶ℋ 𝑥) |
| 20 | 18, 19 | vtoclga 3577 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈
Cℋ → 𝐴 𝐶ℋ 𝑟) |
| 21 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑞 → (𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑞)) |
| 22 | 21, 19 | vtoclga 3577 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈
Cℋ → 𝐴 𝐶ℋ 𝑞) |
| 23 | 20, 22 | anim12i 613 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞)) |
| 24 | | fh1 31637 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
Cℋ ∧ 𝑟 ∈ Cℋ
∧ 𝑞 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
| 25 | 2, 24 | mp3anl1 1457 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
∧ (𝐴
𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
| 26 | 23, 25 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
| 27 | 5, 26 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ HAtoms ∧ 𝑞 ∈
Cℋ ) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
| 28 | 27 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈
Cℋ ∧ 𝑟 ∈ HAtoms) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
| 29 | 28 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝑞 ∈
Cℋ ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴)) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
| 30 | 29 | ad2ant2r 747 |
. . . . . . . . 9
⊢ (((𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
| 31 | 30 | adantll 714 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
| 32 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑝 → (𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑝)) |
| 33 | 32, 19 | vtoclga 3577 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
Cℋ → 𝐴 𝐶ℋ 𝑝) |
| 34 | 33, 22 | anim12i 613 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞)) |
| 35 | | fh1 31637 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
Cℋ ∧ 𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
| 36 | 2, 35 | mp3anl1 1457 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
∧ (𝐴
𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
| 37 | 34, 36 | mpdan 687 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
| 38 | 7, 37 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈
Cℋ ) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
| 39 | 38 | ad2ant2r 747 |
. . . . . . . . 9
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) →
(𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
| 40 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
| 41 | 17, 31, 40 | 3eqtr3d 2785 |
. . . . . . 7
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
| 42 | | sseqin2 4223 |
. . . . . . . . . . 11
⊢ (𝑟 ⊆ 𝐴 ↔ (𝐴 ∩ 𝑟) = 𝑟) |
| 43 | 42 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑟 ⊆ 𝐴 → (𝐴 ∩ 𝑟) = 𝑟) |
| 44 | 43 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝐴 ∩ 𝑟) = 𝑟) |
| 45 | 44 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ 𝑟) = 𝑟) |
| 46 | | incom 4209 |
. . . . . . . . . 10
⊢ (𝐴 ∩ 𝑞) = (𝑞 ∩ 𝐴) |
| 47 | | chsh 31243 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈
Cℋ → 𝑞 ∈ Sℋ
) |
| 48 | 2 | chshii 31246 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈
Sℋ |
| 49 | | orthin 31465 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈
Sℋ ∧ 𝐴 ∈ Sℋ )
→ (𝑞 ⊆
(⊥‘𝐴) →
(𝑞 ∩ 𝐴) = 0ℋ)) |
| 50 | 47, 48, 49 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝑞 ∈
Cℋ → (𝑞 ⊆ (⊥‘𝐴) → (𝑞 ∩ 𝐴) = 0ℋ)) |
| 51 | 50 | imp 406 |
. . . . . . . . . 10
⊢ ((𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) → (𝑞 ∩ 𝐴) = 0ℋ) |
| 52 | 46, 51 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) → (𝐴 ∩ 𝑞) = 0ℋ) |
| 53 | 52 | ad2antlr 727 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ 𝑞) = 0ℋ) |
| 54 | 45, 53 | oveq12d 7449 |
. . . . . . 7
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)) = (𝑟 ∨ℋ
0ℋ)) |
| 55 | | sseqin2 4223 |
. . . . . . . . . . 11
⊢ (𝑝 ⊆ 𝐴 ↔ (𝐴 ∩ 𝑝) = 𝑝) |
| 56 | 55 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑝 ⊆ 𝐴 → (𝐴 ∩ 𝑝) = 𝑝) |
| 57 | 56 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) → (𝐴 ∩ 𝑝) = 𝑝) |
| 58 | 57 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ 𝑝) = 𝑝) |
| 59 | 58, 53 | oveq12d 7449 |
. . . . . . 7
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)) = (𝑝 ∨ℋ
0ℋ)) |
| 60 | 41, 54, 59 | 3eqtr3d 2785 |
. . . . . 6
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ 0ℋ)
= (𝑝 ∨ℋ
0ℋ)) |
| 61 | | chj0 31516 |
. . . . . . . . 9
⊢ (𝑟 ∈
Cℋ → (𝑟 ∨ℋ 0ℋ)
= 𝑟) |
| 62 | 5, 61 | syl 17 |
. . . . . . . 8
⊢ (𝑟 ∈ HAtoms → (𝑟 ∨ℋ
0ℋ) = 𝑟) |
| 63 | 62 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ 0ℋ)
= 𝑟) |
| 64 | 63 | adantl 481 |
. . . . . 6
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ 0ℋ)
= 𝑟) |
| 65 | | chj0 31516 |
. . . . . . . 8
⊢ (𝑝 ∈
Cℋ → (𝑝 ∨ℋ 0ℋ)
= 𝑝) |
| 66 | 7, 65 | syl 17 |
. . . . . . 7
⊢ (𝑝 ∈ HAtoms → (𝑝 ∨ℋ
0ℋ) = 𝑝) |
| 67 | 66 | ad3antrrr 730 |
. . . . . 6
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑝 ∨ℋ 0ℋ)
= 𝑝) |
| 68 | 60, 64, 67 | 3eqtr3d 2785 |
. . . . 5
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → 𝑟 = 𝑝) |
| 69 | 68 | exp44 437 |
. . . 4
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) →
(𝑟 ∈ HAtoms →
(𝑟 ⊆ 𝐴 → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → 𝑟 = 𝑝)))) |
| 70 | 69 | com34 91 |
. . 3
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) →
(𝑟 ∈ HAtoms →
(𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝)))) |
| 71 | 1, 70 | sylanr1 682 |
. 2
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → (𝑟 ∈ HAtoms → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝)))) |
| 72 | 71 | imp32 418 |
1
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝)) |