Proof of Theorem chirredlem3
Step | Hyp | Ref
| Expression |
1 | | atelch 28587 |
. . 3
⊢ (𝑞 ∈ HAtoms → 𝑞 ∈
Cℋ ) |
2 | | chirred.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈
Cℋ |
3 | 2 | chirredlem2 28634 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞)) = 𝑞) |
4 | 3 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑟 ∨ℋ 𝑞)) |
5 | | atelch 28587 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ HAtoms → 𝑟 ∈
Cℋ ) |
6 | 5 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → 𝑟 ∈ Cℋ
) |
7 | | atelch 28587 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ HAtoms → 𝑝 ∈
Cℋ ) |
8 | | chjcl 27600 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝑝
∨ℋ 𝑞)
∈ Cℋ ) |
9 | 7, 8 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈
Cℋ ) → (𝑝 ∨ℋ 𝑞) ∈ Cℋ
) |
10 | 9 | ad2ant2r 779 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) →
(𝑝 ∨ℋ
𝑞) ∈
Cℋ ) |
11 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) |
12 | | pjoml2 27854 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈
Cℋ ∧ (𝑝 ∨ℋ 𝑞) ∈ Cℋ
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞)) |
13 | 6, 10, 11, 12 | syl3an 1360 |
. . . . . . . . . . . 12
⊢ (((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ ((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞)) |
14 | 13 | 3com12 1261 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
(𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞)) |
15 | 14 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ ((⊥‘𝑟) ∩ (𝑝 ∨ℋ 𝑞))) = (𝑝 ∨ℋ 𝑞)) |
16 | 4, 15 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ 𝑞) = (𝑝 ∨ℋ 𝑞)) |
17 | 16 | ineq2d 3776 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = (𝐴 ∩ (𝑝 ∨ℋ 𝑞))) |
18 | | breq2 4587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑟 → (𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑟)) |
19 | | chirred.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈
Cℋ → 𝐴 𝐶ℋ 𝑥) |
20 | 18, 19 | vtoclga 3245 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈
Cℋ → 𝐴 𝐶ℋ 𝑟) |
21 | | breq2 4587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑞 → (𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑞)) |
22 | 21, 19 | vtoclga 3245 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈
Cℋ → 𝐴 𝐶ℋ 𝑞) |
23 | 20, 22 | anim12i 588 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞)) |
24 | | fh1 27861 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
Cℋ ∧ 𝑟 ∈ Cℋ
∧ 𝑞 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
25 | 2, 24 | mp3anl1 1410 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
∧ (𝐴
𝐶ℋ 𝑟 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
26 | 23, 25 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
27 | 5, 26 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ HAtoms ∧ 𝑞 ∈
Cℋ ) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
28 | 27 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈
Cℋ ∧ 𝑟 ∈ HAtoms) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
29 | 28 | adantrr 749 |
. . . . . . . . . 10
⊢ ((𝑞 ∈
Cℋ ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴)) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
30 | 29 | ad2ant2r 779 |
. . . . . . . . 9
⊢ (((𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
31 | 30 | adantll 746 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑟 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞))) |
32 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑝 → (𝐴 𝐶ℋ 𝑥 ↔ 𝐴 𝐶ℋ 𝑝)) |
33 | 32, 19 | vtoclga 3245 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
Cℋ → 𝐴 𝐶ℋ 𝑝) |
34 | 33, 22 | anim12i 588 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝐴
𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞)) |
35 | | fh1 27861 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
Cℋ ∧ 𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ ) ∧ (𝐴 𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
36 | 2, 35 | mp3anl1 1410 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
∧ (𝐴
𝐶ℋ 𝑝 ∧ 𝐴 𝐶ℋ 𝑞)) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
37 | 34, 36 | mpdan 699 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
38 | 7, 37 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈
Cℋ ) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
39 | 38 | ad2ant2r 779 |
. . . . . . . . 9
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) →
(𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
40 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ (𝑝 ∨ℋ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
41 | 17, 31, 40 | 3eqtr3d 2652 |
. . . . . . 7
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)) = ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞))) |
42 | | sseqin2 3779 |
. . . . . . . . . . 11
⊢ (𝑟 ⊆ 𝐴 ↔ (𝐴 ∩ 𝑟) = 𝑟) |
43 | 42 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑟 ⊆ 𝐴 → (𝐴 ∩ 𝑟) = 𝑟) |
44 | 43 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝐴 ∩ 𝑟) = 𝑟) |
45 | 44 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ 𝑟) = 𝑟) |
46 | | incom 3767 |
. . . . . . . . . 10
⊢ (𝐴 ∩ 𝑞) = (𝑞 ∩ 𝐴) |
47 | | chsh 27465 |
. . . . . . . . . . . 12
⊢ (𝑞 ∈
Cℋ → 𝑞 ∈ Sℋ
) |
48 | 2 | chshii 27468 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈
Sℋ |
49 | | orthin 27689 |
. . . . . . . . . . . 12
⊢ ((𝑞 ∈
Sℋ ∧ 𝐴 ∈ Sℋ )
→ (𝑞 ⊆
(⊥‘𝐴) →
(𝑞 ∩ 𝐴) = 0ℋ)) |
50 | 47, 48, 49 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝑞 ∈
Cℋ → (𝑞 ⊆ (⊥‘𝐴) → (𝑞 ∩ 𝐴) = 0ℋ)) |
51 | 50 | imp 444 |
. . . . . . . . . 10
⊢ ((𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) → (𝑞 ∩ 𝐴) = 0ℋ) |
52 | 46, 51 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) → (𝐴 ∩ 𝑞) = 0ℋ) |
53 | 52 | ad2antlr 759 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ 𝑞) = 0ℋ) |
54 | 45, 53 | oveq12d 6567 |
. . . . . . 7
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((𝐴 ∩ 𝑟) ∨ℋ (𝐴 ∩ 𝑞)) = (𝑟 ∨ℋ
0ℋ)) |
55 | | sseqin2 3779 |
. . . . . . . . . . 11
⊢ (𝑝 ⊆ 𝐴 ↔ (𝐴 ∩ 𝑝) = 𝑝) |
56 | 55 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑝 ⊆ 𝐴 → (𝐴 ∩ 𝑝) = 𝑝) |
57 | 56 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) → (𝐴 ∩ 𝑝) = 𝑝) |
58 | 57 | ad2antrr 758 |
. . . . . . . 8
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝐴 ∩ 𝑝) = 𝑝) |
59 | 58, 53 | oveq12d 6567 |
. . . . . . 7
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → ((𝐴 ∩ 𝑝) ∨ℋ (𝐴 ∩ 𝑞)) = (𝑝 ∨ℋ
0ℋ)) |
60 | 41, 54, 59 | 3eqtr3d 2652 |
. . . . . 6
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ 0ℋ)
= (𝑝 ∨ℋ
0ℋ)) |
61 | | chj0 27740 |
. . . . . . . . 9
⊢ (𝑟 ∈
Cℋ → (𝑟 ∨ℋ 0ℋ)
= 𝑟) |
62 | 5, 61 | syl 17 |
. . . . . . . 8
⊢ (𝑟 ∈ HAtoms → (𝑟 ∨ℋ
0ℋ) = 𝑟) |
63 | 62 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ∨ℋ 0ℋ)
= 𝑟) |
64 | 63 | adantl 481 |
. . . . . 6
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ∨ℋ 0ℋ)
= 𝑟) |
65 | | chj0 27740 |
. . . . . . . 8
⊢ (𝑝 ∈
Cℋ → (𝑝 ∨ℋ 0ℋ)
= 𝑝) |
66 | 7, 65 | syl 17 |
. . . . . . 7
⊢ (𝑝 ∈ HAtoms → (𝑝 ∨ℋ
0ℋ) = 𝑝) |
67 | 66 | ad3antrrr 762 |
. . . . . 6
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑝 ∨ℋ 0ℋ)
= 𝑝) |
68 | 60, 64, 67 | 3eqtr3d 2652 |
. . . . 5
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) ∧
((𝑟 ∈ HAtoms ∧
𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → 𝑟 = 𝑝) |
69 | 68 | exp44 639 |
. . . 4
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) →
(𝑟 ∈ HAtoms →
(𝑟 ⊆ 𝐴 → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → 𝑟 = 𝑝)))) |
70 | 69 | com34 89 |
. . 3
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ Cℋ
∧ 𝑞 ⊆
(⊥‘𝐴))) →
(𝑟 ∈ HAtoms →
(𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝)))) |
71 | 1, 70 | sylanr1 682 |
. 2
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → (𝑟 ∈ HAtoms → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝)))) |
72 | 71 | imp32 448 |
1
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 ⊆ 𝐴 → 𝑟 = 𝑝)) |