Proof of Theorem chirredlem1
Step | Hyp | Ref
| Expression |
1 | | atelch 29775 |
. . . . . . 7
⊢ (𝑟 ∈ HAtoms → 𝑟 ∈
Cℋ ) |
2 | | chirred.1 |
. . . . . . . . 9
⊢ 𝐴 ∈
Cℋ |
3 | | chsscon3 28931 |
. . . . . . . . 9
⊢ ((𝑟 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (𝑟 ⊆ 𝐴 ↔ (⊥‘𝐴) ⊆ (⊥‘𝑟))) |
4 | 2, 3 | mpan2 681 |
. . . . . . . 8
⊢ (𝑟 ∈
Cℋ → (𝑟 ⊆ 𝐴 ↔ (⊥‘𝐴) ⊆ (⊥‘𝑟))) |
5 | 4 | biimpa 470 |
. . . . . . 7
⊢ ((𝑟 ∈
Cℋ ∧ 𝑟 ⊆ 𝐴) → (⊥‘𝐴) ⊆ (⊥‘𝑟)) |
6 | 1, 5 | sylan 575 |
. . . . . 6
⊢ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → (⊥‘𝐴) ⊆ (⊥‘𝑟)) |
7 | | sstr2 3828 |
. . . . . 6
⊢ (𝑞 ⊆ (⊥‘𝐴) → ((⊥‘𝐴) ⊆ (⊥‘𝑟) → 𝑞 ⊆ (⊥‘𝑟))) |
8 | 6, 7 | syl5 34 |
. . . . 5
⊢ (𝑞 ⊆ (⊥‘𝐴) → ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → 𝑞 ⊆ (⊥‘𝑟))) |
9 | | atelch 29775 |
. . . . . . . . 9
⊢ (𝑝 ∈ HAtoms → 𝑝 ∈
Cℋ ) |
10 | | atne0 29776 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ HAtoms → 𝑟 ≠
0ℋ) |
11 | 10 | neneqd 2974 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ HAtoms → ¬
𝑟 =
0ℋ) |
12 | 11 | ad3antrrr 720 |
. . . . . . . . . . 11
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 𝑟 = 0ℋ) |
13 | | simplr 759 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) |
14 | | choccl 28737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈
Cℋ → (⊥‘𝑟) ∈ Cℋ
) |
15 | 1, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ HAtoms →
(⊥‘𝑟) ∈
Cℋ ) |
16 | | chlej1 28941 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝 ∈
Cℋ ∧ (⊥‘𝑟) ∈ Cℋ
∧ 𝑞 ∈
Cℋ ) ∧ 𝑝 ⊆ (⊥‘𝑟)) → (𝑝 ∨ℋ 𝑞) ⊆ ((⊥‘𝑟) ∨ℋ 𝑞)) |
17 | 16 | 3exp1 1414 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈
Cℋ → ((⊥‘𝑟) ∈ Cℋ
→ (𝑞 ∈
Cℋ → (𝑝 ⊆ (⊥‘𝑟) → (𝑝 ∨ℋ 𝑞) ⊆ ((⊥‘𝑟) ∨ℋ 𝑞))))) |
18 | 15, 17 | syl5com 31 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ HAtoms → (𝑝 ∈
Cℋ → (𝑞 ∈ Cℋ
→ (𝑝 ⊆
(⊥‘𝑟) →
(𝑝 ∨ℋ
𝑞) ⊆
((⊥‘𝑟)
∨ℋ 𝑞))))) |
19 | 18 | imp42 419 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ HAtoms ∧ (𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑝 ⊆
(⊥‘𝑟)) →
(𝑝 ∨ℋ
𝑞) ⊆
((⊥‘𝑟)
∨ℋ 𝑞)) |
20 | 19 | adantllr 709 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑝 ⊆ (⊥‘𝑟)) → (𝑝 ∨ℋ 𝑞) ⊆ ((⊥‘𝑟) ∨ℋ 𝑞)) |
21 | 20 | adantlr 705 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → (𝑝 ∨ℋ 𝑞) ⊆ ((⊥‘𝑟) ∨ℋ 𝑞)) |
22 | 13, 21 | sstrd 3831 |
. . . . . . . . . . . . . 14
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → 𝑟 ⊆ ((⊥‘𝑟) ∨ℋ 𝑞)) |
23 | | chlejb2 28944 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑞 ∈
Cℋ ∧ (⊥‘𝑟) ∈ Cℋ )
→ (𝑞 ⊆
(⊥‘𝑟) ↔
((⊥‘𝑟)
∨ℋ 𝑞) =
(⊥‘𝑟))) |
24 | 23 | ancoms 452 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊥‘𝑟)
∈ Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝑞 ⊆
(⊥‘𝑟) ↔
((⊥‘𝑟)
∨ℋ 𝑞) =
(⊥‘𝑟))) |
25 | 24 | biimpa 470 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊥‘𝑟)
∈ Cℋ ∧ 𝑞 ∈ Cℋ )
∧ 𝑞 ⊆
(⊥‘𝑟)) →
((⊥‘𝑟)
∨ℋ 𝑞) =
(⊥‘𝑟)) |
26 | 15, 25 | sylanl1 670 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ∈
Cℋ ) ∧ 𝑞 ⊆ (⊥‘𝑟)) → ((⊥‘𝑟) ∨ℋ 𝑞) = (⊥‘𝑟)) |
27 | 26 | an32s 642 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ 𝑞 ∈ Cℋ )
→ ((⊥‘𝑟)
∨ℋ 𝑞) =
(⊥‘𝑟)) |
28 | 27 | adantrl 706 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) → ((⊥‘𝑟) ∨ℋ 𝑞) = (⊥‘𝑟)) |
29 | 28 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → ((⊥‘𝑟) ∨ℋ 𝑞) = (⊥‘𝑟)) |
30 | 22, 29 | sseqtrd 3860 |
. . . . . . . . . . . . 13
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → 𝑟 ⊆ (⊥‘𝑟)) |
31 | 30 | ex 403 |
. . . . . . . . . . . 12
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑝 ⊆ (⊥‘𝑟) → 𝑟 ⊆ (⊥‘𝑟))) |
32 | | chssoc 28927 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈
Cℋ → (𝑟 ⊆ (⊥‘𝑟) ↔ 𝑟 = 0ℋ)) |
33 | 32 | biimpd 221 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈
Cℋ → (𝑟 ⊆ (⊥‘𝑟) → 𝑟 = 0ℋ)) |
34 | 1, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ HAtoms → (𝑟 ⊆ (⊥‘𝑟) → 𝑟 = 0ℋ)) |
35 | 34 | ad3antrrr 720 |
. . . . . . . . . . . 12
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ⊆ (⊥‘𝑟) → 𝑟 = 0ℋ)) |
36 | 31, 35 | syld 47 |
. . . . . . . . . . 11
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑝 ⊆ (⊥‘𝑟) → 𝑟 = 0ℋ)) |
37 | 12, 36 | mtod 190 |
. . . . . . . . . 10
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 𝑝 ⊆ (⊥‘𝑟)) |
38 | 37 | ex 403 |
. . . . . . . . 9
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → ¬ 𝑝 ⊆ (⊥‘𝑟))) |
39 | 9, 38 | sylanr1 672 |
. . . . . . . 8
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ))
→ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → ¬ 𝑝 ⊆ (⊥‘𝑟))) |
40 | | atnssm0 29807 |
. . . . . . . . . . 11
⊢
(((⊥‘𝑟)
∈ Cℋ ∧ 𝑝 ∈ HAtoms) → (¬ 𝑝 ⊆ (⊥‘𝑟) ↔ ((⊥‘𝑟) ∩ 𝑝) = 0ℋ)) |
41 | | incom 4028 |
. . . . . . . . . . . 12
⊢
((⊥‘𝑟)
∩ 𝑝) = (𝑝 ∩ (⊥‘𝑟)) |
42 | 41 | eqeq1i 2783 |
. . . . . . . . . . 11
⊢
(((⊥‘𝑟)
∩ 𝑝) =
0ℋ ↔ (𝑝 ∩ (⊥‘𝑟)) = 0ℋ) |
43 | 40, 42 | syl6bb 279 |
. . . . . . . . . 10
⊢
(((⊥‘𝑟)
∈ Cℋ ∧ 𝑝 ∈ HAtoms) → (¬ 𝑝 ⊆ (⊥‘𝑟) ↔ (𝑝 ∩ (⊥‘𝑟)) = 0ℋ)) |
44 | 15, 43 | sylan 575 |
. . . . . . . . 9
⊢ ((𝑟 ∈ HAtoms ∧ 𝑝 ∈ HAtoms) → (¬
𝑝 ⊆
(⊥‘𝑟) ↔
(𝑝 ∩
(⊥‘𝑟)) =
0ℋ)) |
45 | 44 | ad2ant2r 737 |
. . . . . . . 8
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ))
→ (¬ 𝑝 ⊆
(⊥‘𝑟) ↔
(𝑝 ∩
(⊥‘𝑟)) =
0ℋ)) |
46 | 39, 45 | sylibd 231 |
. . . . . . 7
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ))
→ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ)) |
47 | 46 | exp43 429 |
. . . . . 6
⊢ (𝑟 ∈ HAtoms → (𝑞 ⊆ (⊥‘𝑟) → (𝑝 ∈ HAtoms → (𝑞 ∈ Cℋ
→ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑝 ∩ (⊥‘𝑟)) =
0ℋ))))) |
48 | 47 | adantr 474 |
. . . . 5
⊢ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → (𝑞 ⊆ (⊥‘𝑟) → (𝑝 ∈ HAtoms → (𝑞 ∈ Cℋ
→ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑝 ∩ (⊥‘𝑟)) =
0ℋ))))) |
49 | 8, 48 | sylcom 30 |
. . . 4
⊢ (𝑞 ⊆ (⊥‘𝐴) → ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → (𝑝 ∈ HAtoms → (𝑞 ∈ Cℋ
→ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑝 ∩ (⊥‘𝑟)) =
0ℋ))))) |
50 | 49 | com4t 93 |
. . 3
⊢ (𝑝 ∈ HAtoms → (𝑞 ∈
Cℋ → (𝑞 ⊆ (⊥‘𝐴) → ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑝 ∩ (⊥‘𝑟)) =
0ℋ))))) |
51 | 50 | impd 400 |
. 2
⊢ (𝑝 ∈ HAtoms → ((𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) → ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ)))) |
52 | 51 | imp43 420 |
1
⊢ (((𝑝 ∈ HAtoms ∧ (𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ) |