| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . 3
⊢
0ℋ = 0ℋ |
| 2 | | ioran 986 |
. . . . 5
⊢ (¬
(𝐴 = 0ℋ
∨ (⊥‘𝐴) =
0ℋ) ↔ (¬ 𝐴 = 0ℋ ∧ ¬
(⊥‘𝐴) =
0ℋ)) |
| 3 | | df-ne 2941 |
. . . . . 6
⊢ (𝐴 ≠ 0ℋ ↔
¬ 𝐴 =
0ℋ) |
| 4 | | df-ne 2941 |
. . . . . 6
⊢
((⊥‘𝐴)
≠ 0ℋ ↔ ¬ (⊥‘𝐴) = 0ℋ) |
| 5 | 3, 4 | anbi12i 628 |
. . . . 5
⊢ ((𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ) ↔ (¬ 𝐴 = 0ℋ ∧ ¬
(⊥‘𝐴) =
0ℋ)) |
| 6 | 2, 5 | bitr4i 278 |
. . . 4
⊢ (¬
(𝐴 = 0ℋ
∨ (⊥‘𝐴) =
0ℋ) ↔ (𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ)) |
| 7 | | chirred.1 |
. . . . . . . 8
⊢ 𝐴 ∈
Cℋ |
| 8 | 7 | hatomici 32378 |
. . . . . . 7
⊢ (𝐴 ≠ 0ℋ →
∃𝑝 ∈ HAtoms
𝑝 ⊆ 𝐴) |
| 9 | 7 | choccli 31326 |
. . . . . . . 8
⊢
(⊥‘𝐴)
∈ Cℋ |
| 10 | 9 | hatomici 32378 |
. . . . . . 7
⊢
((⊥‘𝐴)
≠ 0ℋ → ∃𝑞 ∈ HAtoms 𝑞 ⊆ (⊥‘𝐴)) |
| 11 | 8, 10 | anim12i 613 |
. . . . . 6
⊢ ((𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ) → (∃𝑝 ∈ HAtoms 𝑝 ⊆ 𝐴 ∧ ∃𝑞 ∈ HAtoms 𝑞 ⊆ (⊥‘𝐴))) |
| 12 | | reeanv 3229 |
. . . . . 6
⊢
(∃𝑝 ∈
HAtoms ∃𝑞 ∈
HAtoms (𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴)) ↔ (∃𝑝 ∈ HAtoms 𝑝 ⊆ 𝐴 ∧ ∃𝑞 ∈ HAtoms 𝑞 ⊆ (⊥‘𝐴))) |
| 13 | 11, 12 | sylibr 234 |
. . . . 5
⊢ ((𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ) → ∃𝑝 ∈ HAtoms ∃𝑞 ∈ HAtoms (𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴))) |
| 14 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → 𝑝 ∈ HAtoms) |
| 15 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → 𝑞 ∈ HAtoms) |
| 16 | | atelch 32363 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 ∈ HAtoms → 𝑝 ∈
Cℋ ) |
| 17 | | chsscon3 31519 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈
Cℋ ∧ 𝐴 ∈ Cℋ )
→ (𝑝 ⊆ 𝐴 ↔ (⊥‘𝐴) ⊆ (⊥‘𝑝))) |
| 18 | 16, 7, 17 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ HAtoms → (𝑝 ⊆ 𝐴 ↔ (⊥‘𝐴) ⊆ (⊥‘𝑝))) |
| 19 | 18 | biimpa 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) → (⊥‘𝐴) ⊆ (⊥‘𝑝)) |
| 20 | | sstr 3992 |
. . . . . . . . . . . . . 14
⊢ ((𝑞 ⊆ (⊥‘𝐴) ∧ (⊥‘𝐴) ⊆ (⊥‘𝑝)) → 𝑞 ⊆ (⊥‘𝑝)) |
| 21 | 19, 20 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ⊆ (⊥‘𝐴) ∧ (𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴)) → 𝑞 ⊆ (⊥‘𝑝)) |
| 22 | 21 | ancoms 458 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ 𝑞 ⊆ (⊥‘𝐴)) → 𝑞 ⊆ (⊥‘𝑝)) |
| 23 | | atne0 32364 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ HAtoms → 𝑝 ≠
0ℋ) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) → 𝑝 ≠ 0ℋ) |
| 25 | | sseq1 4009 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 𝑞 → (𝑝 ⊆ (⊥‘𝑝) ↔ 𝑞 ⊆ (⊥‘𝑝))) |
| 26 | 25 | bicomd 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 𝑞 → (𝑞 ⊆ (⊥‘𝑝) ↔ 𝑝 ⊆ (⊥‘𝑝))) |
| 27 | | chssoc 31515 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈
Cℋ → (𝑝 ⊆ (⊥‘𝑝) ↔ 𝑝 = 0ℋ)) |
| 28 | 16, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ HAtoms → (𝑝 ⊆ (⊥‘𝑝) ↔ 𝑝 = 0ℋ)) |
| 29 | 26, 28 | sylan9bbr 510 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ HAtoms ∧ 𝑝 = 𝑞) → (𝑞 ⊆ (⊥‘𝑝) ↔ 𝑝 = 0ℋ)) |
| 30 | 29 | biimpa 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 = 𝑞) ∧ 𝑞 ⊆ (⊥‘𝑝)) → 𝑝 = 0ℋ) |
| 31 | 30 | an32s 652 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) ∧ 𝑝 = 𝑞) → 𝑝 = 0ℋ) |
| 32 | 31 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) → (𝑝 = 𝑞 → 𝑝 = 0ℋ)) |
| 33 | 32 | necon3d 2961 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) → (𝑝 ≠ 0ℋ → 𝑝 ≠ 𝑞)) |
| 34 | 24, 33 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝑝)) → 𝑝 ≠ 𝑞) |
| 35 | 34 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ 𝑞 ⊆ (⊥‘𝑝)) → 𝑝 ≠ 𝑞) |
| 36 | 22, 35 | syldan 591 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ 𝑞 ⊆ (⊥‘𝐴)) → 𝑝 ≠ 𝑞) |
| 37 | 36 | adantrl 716 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → 𝑝 ≠ 𝑞) |
| 38 | | superpos 32373 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms ∧ 𝑝 ≠ 𝑞) → ∃𝑟 ∈ HAtoms (𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
| 39 | 14, 15, 37, 38 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → ∃𝑟 ∈ HAtoms (𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
| 40 | | df-3an 1089 |
. . . . . . . . . . . 12
⊢ ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ↔ ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
| 41 | | neanior 3035 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞) ↔ ¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞)) |
| 42 | 41 | anbi1i 624 |
. . . . . . . . . . . 12
⊢ (((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ↔ (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
| 43 | 40, 42 | bitri 275 |
. . . . . . . . . . 11
⊢ ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) ↔ (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) |
| 44 | | chirred.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
Cℋ → 𝐴 𝐶ℋ 𝑥) |
| 45 | 7, 44 | chirredlem4 32412 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞))) → (𝑟 = 𝑝 ∨ 𝑟 = 𝑞)) |
| 46 | 45 | anassrs 467 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑝 ∈ HAtoms
∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (𝑟 = 𝑝 ∨ 𝑟 = 𝑞)) |
| 47 | 46 | pm2.24d 151 |
. . . . . . . . . . . . . 14
⊢
(((((𝑝 ∈ HAtoms
∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) → ¬ 0ℋ =
0ℋ)) |
| 48 | 47 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) → ¬ 0ℋ =
0ℋ))) |
| 49 | 48 | com23 86 |
. . . . . . . . . . . 12
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) → (¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) → (𝑟 ⊆ (𝑝 ∨ℋ 𝑞) → ¬ 0ℋ =
0ℋ))) |
| 50 | 49 | impd 410 |
. . . . . . . . . . 11
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) → ((¬ (𝑟 = 𝑝 ∨ 𝑟 = 𝑞) ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 0ℋ =
0ℋ)) |
| 51 | 43, 50 | biimtrid 242 |
. . . . . . . . . 10
⊢ ((((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ∈ HAtoms) → ((𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 0ℋ =
0ℋ)) |
| 52 | 51 | rexlimdva 3155 |
. . . . . . . . 9
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → (∃𝑟 ∈ HAtoms (𝑟 ≠ 𝑝 ∧ 𝑟 ≠ 𝑞 ∧ 𝑟 ⊆ (𝑝 ∨ℋ 𝑞)) → ¬ 0ℋ =
0ℋ)) |
| 53 | 39, 52 | mpd 15 |
. . . . . . . 8
⊢ (((𝑝 ∈ HAtoms ∧ 𝑝 ⊆ 𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → ¬ 0ℋ =
0ℋ) |
| 54 | 53 | an4s 660 |
. . . . . . 7
⊢ (((𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms) ∧ (𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴))) → ¬ 0ℋ =
0ℋ) |
| 55 | 54 | ex 412 |
. . . . . 6
⊢ ((𝑝 ∈ HAtoms ∧ 𝑞 ∈ HAtoms) → ((𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴)) → ¬ 0ℋ =
0ℋ)) |
| 56 | 55 | rexlimivv 3201 |
. . . . 5
⊢
(∃𝑝 ∈
HAtoms ∃𝑞 ∈
HAtoms (𝑝 ⊆ 𝐴 ∧ 𝑞 ⊆ (⊥‘𝐴)) → ¬ 0ℋ =
0ℋ) |
| 57 | 13, 56 | syl 17 |
. . . 4
⊢ ((𝐴 ≠ 0ℋ ∧
(⊥‘𝐴) ≠
0ℋ) → ¬ 0ℋ =
0ℋ) |
| 58 | 6, 57 | sylbi 217 |
. . 3
⊢ (¬
(𝐴 = 0ℋ
∨ (⊥‘𝐴) =
0ℋ) → ¬ 0ℋ =
0ℋ) |
| 59 | 1, 58 | mt4 116 |
. 2
⊢ (𝐴 = 0ℋ ∨
(⊥‘𝐴) =
0ℋ) |
| 60 | | fveq2 6906 |
. . . 4
⊢
((⊥‘𝐴) =
0ℋ → (⊥‘(⊥‘𝐴)) =
(⊥‘0ℋ)) |
| 61 | 7 | ococi 31424 |
. . . 4
⊢
(⊥‘(⊥‘𝐴)) = 𝐴 |
| 62 | | choc0 31345 |
. . . 4
⊢
(⊥‘0ℋ) = ℋ |
| 63 | 60, 61, 62 | 3eqtr3g 2800 |
. . 3
⊢
((⊥‘𝐴) =
0ℋ → 𝐴 = ℋ) |
| 64 | 63 | orim2i 911 |
. 2
⊢ ((𝐴 = 0ℋ ∨
(⊥‘𝐴) =
0ℋ) → (𝐴 = 0ℋ ∨ 𝐴 = ℋ)) |
| 65 | 59, 64 | ax-mp 5 |
1
⊢ (𝐴 = 0ℋ ∨
𝐴 =
ℋ) |