Proof of Theorem chirredlem1
Step | Hyp | Ref
| Expression |
1 | | atelch 30702 |
. . . . . . 7
⊢ (𝑟 ∈ HAtoms → 𝑟 ∈
Cℋ ) |
2 | | chirred.1 |
. . . . . . . . 9
⊢ 𝐴 ∈
Cℋ |
3 | | chsscon3 29858 |
. . . . . . . . 9
⊢ ((𝑟 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (𝑟 ⊆ 𝐴 ↔ (⊥‘𝐴) ⊆ (⊥‘𝑟))) |
4 | 2, 3 | mpan2 688 |
. . . . . . . 8
⊢ (𝑟 ∈
Cℋ → (𝑟 ⊆ 𝐴 ↔ (⊥‘𝐴) ⊆ (⊥‘𝑟))) |
5 | 4 | biimpa 477 |
. . . . . . 7
⊢ ((𝑟 ∈
Cℋ ∧ 𝑟 ⊆ 𝐴) → (⊥‘𝐴) ⊆ (⊥‘𝑟)) |
6 | 1, 5 | sylan 580 |
. . . . . 6
⊢ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → (⊥‘𝐴) ⊆ (⊥‘𝑟)) |
7 | | sstr2 3933 |
. . . . . 6
⊢ (𝑞 ⊆ (⊥‘𝐴) → ((⊥‘𝐴) ⊆ (⊥‘𝑟) → 𝑞 ⊆ (⊥‘𝑟))) |
8 | 6, 7 | syl5 34 |
. . . . 5
⊢ (𝑞 ⊆ (⊥‘𝐴) → ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → 𝑞 ⊆ (⊥‘𝑟))) |
9 | | atelch 30702 |
. . . . . . . . 9
⊢ (𝑝 ∈ HAtoms → 𝑝 ∈
Cℋ ) |
10 | | atne0 30703 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ HAtoms → 𝑟 ≠
0ℋ) |
11 | 10 | neneqd 2950 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ HAtoms → ¬
𝑟 =
0ℋ) |
12 | 11 | ad3antrrr 727 |
. . . . . . . . . . 11
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 𝑟 = 0ℋ) |
13 | | simplr 766 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) |
14 | | choccl 29664 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈
Cℋ → (⊥‘𝑟) ∈ Cℋ
) |
15 | 1, 14 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑟 ∈ HAtoms →
(⊥‘𝑟) ∈
Cℋ ) |
16 | | chlej1 29868 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝 ∈
Cℋ ∧ (⊥‘𝑟) ∈ Cℋ
∧ 𝑞 ∈
Cℋ ) ∧ 𝑝 ⊆ (⊥‘𝑟)) → (𝑝 ∨ℋ 𝑞) ⊆ ((⊥‘𝑟) ∨ℋ 𝑞)) |
17 | 16 | 3exp1 1351 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈
Cℋ → ((⊥‘𝑟) ∈ Cℋ
→ (𝑞 ∈
Cℋ → (𝑝 ⊆ (⊥‘𝑟) → (𝑝 ∨ℋ 𝑞) ⊆ ((⊥‘𝑟) ∨ℋ 𝑞))))) |
18 | 15, 17 | syl5com 31 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ HAtoms → (𝑝 ∈
Cℋ → (𝑞 ∈ Cℋ
→ (𝑝 ⊆
(⊥‘𝑟) →
(𝑝 ∨ℋ
𝑞) ⊆
((⊥‘𝑟)
∨ℋ 𝑞))))) |
19 | 18 | imp42 427 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ HAtoms ∧ (𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑝 ⊆
(⊥‘𝑟)) →
(𝑝 ∨ℋ
𝑞) ⊆
((⊥‘𝑟)
∨ℋ 𝑞)) |
20 | 19 | adantllr 716 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑝 ⊆ (⊥‘𝑟)) → (𝑝 ∨ℋ 𝑞) ⊆ ((⊥‘𝑟) ∨ℋ 𝑞)) |
21 | 20 | adantlr 712 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → (𝑝 ∨ℋ 𝑞) ⊆ ((⊥‘𝑟) ∨ℋ 𝑞)) |
22 | 13, 21 | sstrd 3936 |
. . . . . . . . . . . . . 14
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → 𝑟 ⊆ ((⊥‘𝑟) ∨ℋ 𝑞)) |
23 | | chlejb2 29871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑞 ∈
Cℋ ∧ (⊥‘𝑟) ∈ Cℋ )
→ (𝑞 ⊆
(⊥‘𝑟) ↔
((⊥‘𝑟)
∨ℋ 𝑞) =
(⊥‘𝑟))) |
24 | 23 | ancoms 459 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊥‘𝑟)
∈ Cℋ ∧ 𝑞 ∈ Cℋ )
→ (𝑞 ⊆
(⊥‘𝑟) ↔
((⊥‘𝑟)
∨ℋ 𝑞) =
(⊥‘𝑟))) |
25 | 24 | biimpa 477 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊥‘𝑟)
∈ Cℋ ∧ 𝑞 ∈ Cℋ )
∧ 𝑞 ⊆
(⊥‘𝑟)) →
((⊥‘𝑟)
∨ℋ 𝑞) =
(⊥‘𝑟)) |
26 | 15, 25 | sylanl1 677 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ∈
Cℋ ) ∧ 𝑞 ⊆ (⊥‘𝑟)) → ((⊥‘𝑟) ∨ℋ 𝑞) = (⊥‘𝑟)) |
27 | 26 | an32s 649 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ 𝑞 ∈ Cℋ )
→ ((⊥‘𝑟)
∨ℋ 𝑞) =
(⊥‘𝑟)) |
28 | 27 | adantrl 713 |
. . . . . . . . . . . . . . 15
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) → ((⊥‘𝑟) ∨ℋ 𝑞) = (⊥‘𝑟)) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → ((⊥‘𝑟) ∨ℋ 𝑞) = (⊥‘𝑟)) |
30 | 22, 29 | sseqtrd 3966 |
. . . . . . . . . . . . 13
⊢
(((((𝑟 ∈ HAtoms
∧ 𝑞 ⊆
(⊥‘𝑟)) ∧
(𝑝 ∈
Cℋ ∧ 𝑞 ∈ Cℋ ))
∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ∧ 𝑝 ⊆ (⊥‘𝑟)) → 𝑟 ⊆ (⊥‘𝑟)) |
31 | 30 | ex 413 |
. . . . . . . . . . . 12
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑝 ⊆ (⊥‘𝑟) → 𝑟 ⊆ (⊥‘𝑟))) |
32 | | chssoc 29854 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈
Cℋ → (𝑟 ⊆ (⊥‘𝑟) ↔ 𝑟 = 0ℋ)) |
33 | 32 | biimpd 228 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈
Cℋ → (𝑟 ⊆ (⊥‘𝑟) → 𝑟 = 0ℋ)) |
34 | 1, 33 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ HAtoms → (𝑟 ⊆ (⊥‘𝑟) → 𝑟 = 0ℋ)) |
35 | 34 | ad3antrrr 727 |
. . . . . . . . . . . 12
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 ⊆ (⊥‘𝑟) → 𝑟 = 0ℋ)) |
36 | 31, 35 | syld 47 |
. . . . . . . . . . 11
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑝 ⊆ (⊥‘𝑟) → 𝑟 = 0ℋ)) |
37 | 12, 36 | mtod 197 |
. . . . . . . . . 10
⊢ ((((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 𝑝 ⊆ (⊥‘𝑟)) |
38 | 37 | ex 413 |
. . . . . . . . 9
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ Cℋ
∧ 𝑞 ∈
Cℋ )) → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → ¬ 𝑝 ⊆ (⊥‘𝑟))) |
39 | 9, 38 | sylanr1 679 |
. . . . . . . 8
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ))
→ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → ¬ 𝑝 ⊆ (⊥‘𝑟))) |
40 | | atnssm0 30734 |
. . . . . . . . . . 11
⊢
(((⊥‘𝑟)
∈ Cℋ ∧ 𝑝 ∈ HAtoms) → (¬ 𝑝 ⊆ (⊥‘𝑟) ↔ ((⊥‘𝑟) ∩ 𝑝) = 0ℋ)) |
41 | | incom 4140 |
. . . . . . . . . . . 12
⊢
((⊥‘𝑟)
∩ 𝑝) = (𝑝 ∩ (⊥‘𝑟)) |
42 | 41 | eqeq1i 2745 |
. . . . . . . . . . 11
⊢
(((⊥‘𝑟)
∩ 𝑝) =
0ℋ ↔ (𝑝 ∩ (⊥‘𝑟)) = 0ℋ) |
43 | 40, 42 | bitrdi 287 |
. . . . . . . . . 10
⊢
(((⊥‘𝑟)
∈ Cℋ ∧ 𝑝 ∈ HAtoms) → (¬ 𝑝 ⊆ (⊥‘𝑟) ↔ (𝑝 ∩ (⊥‘𝑟)) = 0ℋ)) |
44 | 15, 43 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑟 ∈ HAtoms ∧ 𝑝 ∈ HAtoms) → (¬
𝑝 ⊆
(⊥‘𝑟) ↔
(𝑝 ∩
(⊥‘𝑟)) =
0ℋ)) |
45 | 44 | ad2ant2r 744 |
. . . . . . . 8
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ))
→ (¬ 𝑝 ⊆
(⊥‘𝑟) ↔
(𝑝 ∩
(⊥‘𝑟)) =
0ℋ)) |
46 | 39, 45 | sylibd 238 |
. . . . . . 7
⊢ (((𝑟 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑟)) ∧ (𝑝 ∈ HAtoms ∧ 𝑞 ∈ Cℋ ))
→ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ)) |
47 | 46 | exp43 437 |
. . . . . 6
⊢ (𝑟 ∈ HAtoms → (𝑞 ⊆ (⊥‘𝑟) → (𝑝 ∈ HAtoms → (𝑞 ∈ Cℋ
→ (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑝 ∩ (⊥‘𝑟)) =
0ℋ))))) |
48 | 47 | adantr 481 |
. . . . 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 411 |
. 2
⊢ (𝑝 ∈ HAtoms → ((𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴)) → ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ)))) |
52 | 51 | imp43 428 |
1
⊢ (((𝑝 ∈ HAtoms ∧ (𝑞 ∈
Cℋ ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟 ⊆ 𝐴) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑝 ∩ (⊥‘𝑟)) = 0ℋ) |