| Step | Hyp | Ref
| Expression |
| 1 | | elat2 32359 |
. . . 4
⊢ (𝐴 ∈ HAtoms ↔ (𝐴 ∈
Cℋ ∧ (𝐴 ≠ 0ℋ ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ))))) |
| 2 | | chne0 31513 |
. . . . . 6
⊢ (𝐴 ∈
Cℋ → (𝐴 ≠ 0ℋ ↔
∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ)) |
| 3 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑥 𝐴 ∈
Cℋ |
| 4 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)) |
| 5 | | nfre1 3285 |
. . . . . . . 8
⊢
Ⅎ𝑥∃𝑥 ∈ ℋ (𝑥 ≠ 0ℎ ∧
𝐴 =
(⊥‘(⊥‘{𝑥}))) |
| 6 | 4, 5 | nfim 1896 |
. . . . . . 7
⊢
Ⅎ𝑥(∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)) → ∃𝑥 ∈ ℋ (𝑥 ≠ 0ℎ ∧
𝐴 =
(⊥‘(⊥‘{𝑥})))) |
| 7 | | chel 31249 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℋ) |
| 8 | 7 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
Cℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ)) → 𝑥 ∈
ℋ) |
| 9 | 8 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝐴 ∈
Cℋ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ) ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) → 𝑥 ∈
ℋ) |
| 10 | | simprlr 780 |
. . . . . . . . 9
⊢ ((𝐴 ∈
Cℋ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ) ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) → 𝑥 ≠
0ℎ) |
| 11 | | h1dn0 31571 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℋ ∧ 𝑥 ≠ 0ℎ)
→ (⊥‘(⊥‘{𝑥})) ≠
0ℋ) |
| 12 | 7, 11 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
Cℋ ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 ≠ 0ℎ) →
(⊥‘(⊥‘{𝑥})) ≠
0ℋ) |
| 13 | 12 | anasss 466 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
Cℋ ∧ (𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ)) →
(⊥‘(⊥‘{𝑥})) ≠
0ℋ) |
| 14 | 13 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
Cℋ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ) ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) →
(⊥‘(⊥‘{𝑥})) ≠
0ℋ) |
| 15 | | ch1dle 32371 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ 𝐴) →
(⊥‘(⊥‘{𝑥})) ⊆ 𝐴) |
| 16 | | snssi 4808 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℋ → {𝑥} ⊆
ℋ) |
| 17 | | occl 31323 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑥} ⊆ ℋ →
(⊥‘{𝑥}) ∈
Cℋ ) |
| 18 | 7, 16, 17 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ 𝐴) → (⊥‘{𝑥}) ∈ Cℋ
) |
| 19 | | choccl 31325 |
. . . . . . . . . . . . . . . . 17
⊢
((⊥‘{𝑥})
∈ Cℋ →
(⊥‘(⊥‘{𝑥})) ∈ Cℋ
) |
| 20 | | sseq1 4009 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 =
(⊥‘(⊥‘{𝑥})) → (𝑦 ⊆ 𝐴 ↔ (⊥‘(⊥‘{𝑥})) ⊆ 𝐴)) |
| 21 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 =
(⊥‘(⊥‘{𝑥})) → (𝑦 = 𝐴 ↔ (⊥‘(⊥‘{𝑥})) = 𝐴)) |
| 22 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 =
(⊥‘(⊥‘{𝑥})) → (𝑦 = 0ℋ ↔
(⊥‘(⊥‘{𝑥})) = 0ℋ)) |
| 23 | 21, 22 | orbi12d 919 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 =
(⊥‘(⊥‘{𝑥})) → ((𝑦 = 𝐴 ∨ 𝑦 = 0ℋ) ↔
((⊥‘(⊥‘{𝑥})) = 𝐴 ∨ (⊥‘(⊥‘{𝑥})) =
0ℋ))) |
| 24 | 20, 23 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 =
(⊥‘(⊥‘{𝑥})) → ((𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)) ↔
((⊥‘(⊥‘{𝑥})) ⊆ 𝐴 →
((⊥‘(⊥‘{𝑥})) = 𝐴 ∨ (⊥‘(⊥‘{𝑥})) =
0ℋ)))) |
| 25 | 24 | rspcv 3618 |
. . . . . . . . . . . . . . . . 17
⊢
((⊥‘(⊥‘{𝑥})) ∈ Cℋ
→ (∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)) →
((⊥‘(⊥‘{𝑥})) ⊆ 𝐴 →
((⊥‘(⊥‘{𝑥})) = 𝐴 ∨ (⊥‘(⊥‘{𝑥})) =
0ℋ)))) |
| 26 | 18, 19, 25 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)) →
((⊥‘(⊥‘{𝑥})) ⊆ 𝐴 →
((⊥‘(⊥‘{𝑥})) = 𝐴 ∨ (⊥‘(⊥‘{𝑥})) =
0ℋ)))) |
| 27 | 15, 26 | mpid 44 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈
Cℋ ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)) →
((⊥‘(⊥‘{𝑥})) = 𝐴 ∨ (⊥‘(⊥‘{𝑥})) =
0ℋ))) |
| 28 | 27 | impr 454 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
Cℋ ∧ (𝑥 ∈ 𝐴 ∧ ∀𝑦 ∈ Cℋ
(𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) →
((⊥‘(⊥‘{𝑥})) = 𝐴 ∨ (⊥‘(⊥‘{𝑥})) =
0ℋ)) |
| 29 | 28 | adantrlr 723 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ) ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) →
((⊥‘(⊥‘{𝑥})) = 𝐴 ∨ (⊥‘(⊥‘{𝑥})) =
0ℋ)) |
| 30 | 29 | ord 865 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
Cℋ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ) ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) → (¬
(⊥‘(⊥‘{𝑥})) = 𝐴 → (⊥‘(⊥‘{𝑥})) =
0ℋ)) |
| 31 | | nne 2944 |
. . . . . . . . . . . 12
⊢ (¬
(⊥‘(⊥‘{𝑥})) ≠ 0ℋ ↔
(⊥‘(⊥‘{𝑥})) = 0ℋ) |
| 32 | 30, 31 | imbitrrdi 252 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
Cℋ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ) ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) → (¬
(⊥‘(⊥‘{𝑥})) = 𝐴 → ¬
(⊥‘(⊥‘{𝑥})) ≠
0ℋ)) |
| 33 | 14, 32 | mt4d 117 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
Cℋ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ) ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) →
(⊥‘(⊥‘{𝑥})) = 𝐴) |
| 34 | 33 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝐴 ∈
Cℋ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ) ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) → 𝐴 =
(⊥‘(⊥‘{𝑥}))) |
| 35 | | rspe 3249 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℋ ∧ (𝑥 ≠ 0ℎ ∧
𝐴 =
(⊥‘(⊥‘{𝑥})))) → ∃𝑥 ∈ ℋ (𝑥 ≠ 0ℎ ∧ 𝐴 =
(⊥‘(⊥‘{𝑥})))) |
| 36 | 9, 10, 34, 35 | syl12anc 837 |
. . . . . . . 8
⊢ ((𝐴 ∈
Cℋ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≠ 0ℎ) ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) →
∃𝑥 ∈ ℋ
(𝑥 ≠
0ℎ ∧ 𝐴 = (⊥‘(⊥‘{𝑥})))) |
| 37 | 36 | exp44 437 |
. . . . . . 7
⊢ (𝐴 ∈
Cℋ → (𝑥 ∈ 𝐴 → (𝑥 ≠ 0ℎ →
(∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)) → ∃𝑥 ∈ ℋ (𝑥 ≠ 0ℎ ∧
𝐴 =
(⊥‘(⊥‘{𝑥}))))))) |
| 38 | 3, 6, 37 | rexlimd 3266 |
. . . . . 6
⊢ (𝐴 ∈
Cℋ → (∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ →
(∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)) → ∃𝑥 ∈ ℋ (𝑥 ≠ 0ℎ ∧
𝐴 =
(⊥‘(⊥‘{𝑥})))))) |
| 39 | 2, 38 | sylbid 240 |
. . . . 5
⊢ (𝐴 ∈
Cℋ → (𝐴 ≠ 0ℋ →
(∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)) → ∃𝑥 ∈ ℋ (𝑥 ≠ 0ℎ ∧
𝐴 =
(⊥‘(⊥‘{𝑥})))))) |
| 40 | 39 | imp32 418 |
. . . 4
⊢ ((𝐴 ∈
Cℋ ∧ (𝐴 ≠ 0ℋ ∧
∀𝑦 ∈
Cℋ (𝑦 ⊆ 𝐴 → (𝑦 = 𝐴 ∨ 𝑦 = 0ℋ)))) →
∃𝑥 ∈ ℋ
(𝑥 ≠
0ℎ ∧ 𝐴 = (⊥‘(⊥‘{𝑥})))) |
| 41 | 1, 40 | sylbi 217 |
. . 3
⊢ (𝐴 ∈ HAtoms →
∃𝑥 ∈ ℋ
(𝑥 ≠
0ℎ ∧ 𝐴 = (⊥‘(⊥‘{𝑥})))) |
| 42 | | h1da 32368 |
. . . . . . 7
⊢ ((𝑥 ∈ ℋ ∧ 𝑥 ≠ 0ℎ)
→ (⊥‘(⊥‘{𝑥})) ∈ HAtoms) |
| 43 | | eleq1 2829 |
. . . . . . 7
⊢ (𝐴 =
(⊥‘(⊥‘{𝑥})) → (𝐴 ∈ HAtoms ↔
(⊥‘(⊥‘{𝑥})) ∈ HAtoms)) |
| 44 | 42, 43 | imbitrrid 246 |
. . . . . 6
⊢ (𝐴 =
(⊥‘(⊥‘{𝑥})) → ((𝑥 ∈ ℋ ∧ 𝑥 ≠ 0ℎ) → 𝐴 ∈
HAtoms)) |
| 45 | 44 | expdcom 414 |
. . . . 5
⊢ (𝑥 ∈ ℋ → (𝑥 ≠ 0ℎ
→ (𝐴 =
(⊥‘(⊥‘{𝑥})) → 𝐴 ∈ HAtoms))) |
| 46 | 45 | impd 410 |
. . . 4
⊢ (𝑥 ∈ ℋ → ((𝑥 ≠ 0ℎ ∧
𝐴 =
(⊥‘(⊥‘{𝑥}))) → 𝐴 ∈ HAtoms)) |
| 47 | 46 | rexlimiv 3148 |
. . 3
⊢
(∃𝑥 ∈
ℋ (𝑥 ≠
0ℎ ∧ 𝐴 = (⊥‘(⊥‘{𝑥}))) → 𝐴 ∈ HAtoms) |
| 48 | 41, 47 | impbii 209 |
. 2
⊢ (𝐴 ∈ HAtoms ↔
∃𝑥 ∈ ℋ
(𝑥 ≠
0ℎ ∧ 𝐴 = (⊥‘(⊥‘{𝑥})))) |
| 49 | | spansn 31578 |
. . . . 5
⊢ (𝑥 ∈ ℋ →
(span‘{𝑥}) =
(⊥‘(⊥‘{𝑥}))) |
| 50 | 49 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 ∈ ℋ → (𝐴 = (span‘{𝑥}) ↔ 𝐴 = (⊥‘(⊥‘{𝑥})))) |
| 51 | 50 | anbi2d 630 |
. . 3
⊢ (𝑥 ∈ ℋ → ((𝑥 ≠ 0ℎ ∧
𝐴 = (span‘{𝑥})) ↔ (𝑥 ≠ 0ℎ ∧ 𝐴 =
(⊥‘(⊥‘{𝑥}))))) |
| 52 | 51 | rexbiia 3092 |
. 2
⊢
(∃𝑥 ∈
ℋ (𝑥 ≠
0ℎ ∧ 𝐴 = (span‘{𝑥})) ↔ ∃𝑥 ∈ ℋ (𝑥 ≠ 0ℎ ∧ 𝐴 =
(⊥‘(⊥‘{𝑥})))) |
| 53 | 48, 52 | bitr4i 278 |
1
⊢ (𝐴 ∈ HAtoms ↔
∃𝑥 ∈ ℋ
(𝑥 ≠
0ℎ ∧ 𝐴 = (span‘{𝑥}))) |