Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢
0ℋ = 0ℋ |
2 | | ioran 511 |
. . . . 5
⊢ (¬
(𝐴 = 0ℋ
∨ (⊥‘𝐴) =
0ℋ) ↔ (¬ 𝐴 = 0ℋ ∧ ¬
(⊥‘𝐴) =
0ℋ)) |
3 | | df-ne 2795 |
. . . . . 6
⊢ (𝐴 ≠ 0ℋ ↔
¬ 𝐴 =
0ℋ) |
4 | | df-ne 2795 |
. . . . . 6
⊢
((⊥‘𝐴)
≠ 0ℋ ↔ ¬ (⊥‘𝐴) = 0ℋ) |
5 | 3, 4 | anbi12i 733 |
. . . . 5
⊢ ((𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ) ↔ (¬ 𝐴 = 0ℋ ∧ ¬
(⊥‘𝐴) =
0ℋ)) |
6 | 2, 5 | bitr4i 267 |
. . . 4
⊢ (¬
(𝐴 = 0ℋ
∨ (⊥‘𝐴) =
0ℋ) ↔ (𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ)) |
7 | | chirred.1 |
. . . . . . . 8
⊢ 𝐴 ∈
Cℋ |
8 | 7 | hatomici 29218 |
. . . . . . 7
⊢ (𝐴 ≠ 0ℋ →
∃𝑝 ∈ HAtoms
𝑝 ⊆ 𝐴) |
9 | 7 | choccli 28166 |
. . . . . . . 8
⊢
(⊥‘𝐴)
∈ Cℋ |
10 | 9 | hatomici 29218 |
. . . . . . 7
⊢
((⊥‘𝐴)
≠ 0ℋ → ∃𝑞 ∈ HAtoms 𝑞 ⊆ (⊥‘𝐴)) |
11 | 8, 10 | anim12i 590 |
. . . . . 6
⊢ ((𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ) → (∃𝑝 ∈ HAtoms 𝑝 ⊆ 𝐴 ∧ ∃𝑞 ∈ HAtoms 𝑞 ⊆ (⊥‘𝐴))) |
12 | | reeanv 3107 |
. . . . . 6
⊢
(∃𝑝 ∈
HAtoms ∃𝑞 ∈
HAtoms (𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴)) ↔ (∃𝑝 ∈ HAtoms 𝑝 ⊆ 𝐴 ∧ ∃𝑞 ∈ HAtoms 𝑞 ⊆ (⊥‘𝐴))) |
13 | 11, 12 | sylibr 224 |
. . . . 5
⊢ ((𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ) → ∃𝑝 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴))) |
14 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → 𝑝 ∈ HAtoms) |
15 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → 𝑞 ∈ HAtoms) |
16 | | atelch 29203 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ HAtoms → 𝑝 ∈
Cℋ ) |
17 | | chsscon3 28359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (𝑝 ⊆ 𝐴 ↔ (⊥‘𝐴) ⊆ (⊥‘𝑝))) |
18 | 16, 7, 17 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ HAtoms → (𝑝 ⊆ 𝐴 ↔ (⊥‘𝐴) ⊆ (⊥‘𝑝))) |
19 | 18 | biimpa 501 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) → (⊥‘𝐴) ⊆ (⊥‘𝑝)) |
20 | | sstr 3611 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ⊆ (⊥‘𝐴) ∧ (⊥‘𝐴) ⊆ (⊥‘𝑝)) → 𝑞 ⊆ (⊥‘𝑝)) |
21 | 19, 20 | sylan2 491 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ⊆ (⊥‘𝐴) ∧ (𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴)) → 𝑞 ⊆ (⊥‘𝑝)) |
22 | 21 | ancoms 469 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ 𝑞 ⊆ (⊥‘𝐴)) → 𝑞 ⊆ (⊥‘𝑝)) |
23 | | atne0 29204 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ HAtoms → 𝑝 ≠
0ℋ) |
24 | 23 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) → 𝑝 ≠ 0ℋ) |
25 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 𝑞 → (𝑝 ⊆ (⊥‘𝑝) ↔ 𝑞 ⊆ (⊥‘𝑝))) |
26 | 25 | bicomd 213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 𝑞 → (𝑞 ⊆ (⊥‘𝑝) ↔ 𝑝 ⊆ (⊥‘𝑝))) |
27 | | chssoc 28355 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈
Cℋ → (𝑝 ⊆ (⊥‘𝑝) ↔ 𝑝 = 0ℋ)) |
28 | 16, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ HAtoms → (𝑝 ⊆ (⊥‘𝑝) ↔ 𝑝 = 0ℋ)) |
29 | 26, 28 | sylan9bbr 737 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ HAtoms ∧ 𝑝 = 𝑞) → (𝑞 ⊆ (⊥‘𝑝) ↔ 𝑝 = 0ℋ)) |
30 | 29 | biimpa 501 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 = 𝑞) ∧ 𝑞 ⊆ (⊥‘𝑝)) → 𝑝 = 0ℋ) |
31 | 30 | an32s 846 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) ∧ 𝑝 = 𝑞) → 𝑝 = 0ℋ) |
32 | 31 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) → (𝑝 = 𝑞 → 𝑝 = 0ℋ)) |
33 | 32 | necon3d 2815 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) → (𝑝 ≠ 0ℋ → 𝑝 ≠ 𝑞)) |
34 | 24, 33 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) → 𝑝 ≠ 𝑞) |
35 | 34 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ 𝑞 ⊆ (⊥‘𝑝)) → 𝑝 ≠ 𝑞) |
36 | 22, 35 | syldan 487 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ 𝑞 ⊆ (⊥‘𝐴)) → 𝑝 ≠ 𝑞) |
37 | 36 | adantrl 752 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → 𝑝 ≠ 𝑞) |
38 | | superpos 29213 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms ∧ 𝑝 ≠ 𝑞) → ∃𝑟 ∈ HAtoms (𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
39 | 14, 15, 37, 38 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → ∃𝑟 ∈ HAtoms (𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
40 | | df-3an 1039 |
. . . . . . . . . . . 12
⊢ ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ↔ ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
41 | | neanior 2886 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞) ↔ ¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞)) |
42 | 41 | anbi1i 731 |
. . . . . . . . . . . 12
⊢ (((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ↔ (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
43 | 40, 42 | bitri 264 |
. . . . . . . . . . 11
⊢ ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ↔ (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
44 | | chirred.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
Cℋ → 𝐴 𝐶ℋ 𝑥) |
45 | 7, 44 | chirredlem4 29252 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 = 𝑝 ∨ 𝑟 = 𝑞)) |
46 | 45 | anassrs 680 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑝 ∈ HAtoms
∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 = 𝑝 ∨ 𝑟 = 𝑞)) |
47 | 46 | pm2.24d 147 |
. . . . . . . . . . . . . 14
⊢
(((((𝑝 ∈ HAtoms
∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) → ¬ 0ℋ =
0ℋ)) |
48 | 47 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) → ¬ 0ℋ =
0ℋ))) |
49 | 48 | com23 86 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) → (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → ¬ 0ℋ =
0ℋ))) |
50 | 49 | impd 447 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) → ((¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 0ℋ =
0ℋ)) |
51 | 43, 50 | syl5bi 232 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) → ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 0ℋ =
0ℋ)) |
52 | 51 | rexlimdva 3031 |
. . . . . . . . 9
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → (∃𝑟 ∈ HAtoms (𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 0ℋ =
0ℋ)) |
53 | 39, 52 | mpd 15 |
. . . . . . . 8
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → ¬ 0ℋ =
0ℋ) |
54 | 53 | an4s 869 |
. . . . . . 7
⊢ (((𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms) ∧ (𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴))) → ¬ 0ℋ =
0ℋ) |
55 | 54 | ex 450 |
. . . . . 6
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms) → ((𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴)) → ¬ 0ℋ =
0ℋ)) |
56 | 55 | rexlimivv 3036 |
. . . . 5
⊢
(∃𝑝 ∈
HAtoms ∃𝑞 ∈
HAtoms (𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴)) → ¬ 0ℋ =
0ℋ) |
57 | 13, 56 | syl 17 |
. . . 4
⊢ ((𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ) → ¬ 0ℋ =
0ℋ) |
58 | 6, 57 | sylbi 207 |
. . 3
⊢ (¬
(𝐴 = 0ℋ
∨ (⊥‘𝐴) =
0ℋ) → ¬ 0ℋ =
0ℋ) |
59 | 1, 58 | mt4 115 |
. 2
⊢ (𝐴 = 0ℋ ∨
(⊥‘𝐴) =
0ℋ) |
60 | | fveq2 6191 |
. . . 4
⊢
((⊥‘𝐴) =
0ℋ → (⊥‘(⊥‘𝐴)) =
(⊥‘0ℋ)) |
61 | 7 | ococi 28264 |
. . . 4
⊢
(⊥‘(⊥‘𝐴)) = 𝐴 |
62 | | choc0 28185 |
. . . 4
⊢
(⊥‘0ℋ) = ℋ |
63 | 60, 61, 62 | 3eqtr3g 2679 |
. . 3
⊢
((⊥‘𝐴) =
0ℋ → 𝐴 = ℋ) |
64 | 63 | orim2i 540 |
. 2
⊢ ((𝐴 = 0ℋ ∨
(⊥‘𝐴) =
0ℋ) → (𝐴 = 0ℋ ∨ 𝐴 = ℋ)) |
65 | 59, 64 | ax-mp 5 |
1
⊢ (𝐴 = 0ℋ ∨
𝐴 =
ℋ) |