Step | Hyp | Ref
| Expression |
1 | | opeq1 4874 |
. . . . 5
⊢ (𝑥 = 𝐴 → ⟨𝑥, ℂ⟩ = ⟨𝐴, ℂ⟩) |
2 | | df-bj-inftyexpi 36088 |
. . . . 5
⊢
+∞ei = (𝑥 ∈ (-π(,]π) ↦ ⟨𝑥,
ℂ⟩) |
3 | | opex 5465 |
. . . . 5
⊢
⟨𝐴,
ℂ⟩ ∈ V |
4 | 1, 2, 3 | fvmpt 6999 |
. . . 4
⊢ (𝐴 ∈ (-π(,]π) →
(+∞ei‘𝐴) = ⟨𝐴, ℂ⟩) |
5 | | opex 5465 |
. . . . 5
⊢
⟨𝑥,
ℂ⟩ ∈ V |
6 | 5, 2 | dmmpti 6695 |
. . . 4
⊢ dom
+∞ei = (-π(,]π) |
7 | 4, 6 | eleq2s 2852 |
. . 3
⊢ (𝐴 ∈ dom
+∞ei → (+∞ei‘𝐴) = ⟨𝐴, ℂ⟩) |
8 | | cnex 11191 |
. . . . . . 7
⊢ ℂ
∈ V |
9 | 8 | prid2 4768 |
. . . . . 6
⊢ ℂ
∈ {𝐴,
ℂ} |
10 | | eqid 2733 |
. . . . . . . 8
⊢ {𝐴, ℂ} = {𝐴, ℂ} |
11 | 10 | olci 865 |
. . . . . . 7
⊢ ({𝐴, ℂ} = {𝐴} ∨ {𝐴, ℂ} = {𝐴, ℂ}) |
12 | | elopg 5467 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ ℂ ∈
V) → ({𝐴, ℂ}
∈ ⟨𝐴,
ℂ⟩ ↔ ({𝐴,
ℂ} = {𝐴} ∨ {𝐴, ℂ} = {𝐴, ℂ}))) |
13 | 8, 12 | mpan2 690 |
. . . . . . 7
⊢ (𝐴 ∈ V → ({𝐴, ℂ} ∈ ⟨𝐴, ℂ⟩ ↔ ({𝐴, ℂ} = {𝐴} ∨ {𝐴, ℂ} = {𝐴, ℂ}))) |
14 | 11, 13 | mpbiri 258 |
. . . . . 6
⊢ (𝐴 ∈ V → {𝐴, ℂ} ∈ ⟨𝐴,
ℂ⟩) |
15 | | en3lp 9609 |
. . . . . . 7
⊢ ¬
(ℂ ∈ {𝐴,
ℂ} ∧ {𝐴, ℂ}
∈ ⟨𝐴,
ℂ⟩ ∧ ⟨𝐴, ℂ⟩ ∈
ℂ) |
16 | 15 | bj-imn3ani 35465 |
. . . . . 6
⊢ ((ℂ
∈ {𝐴, ℂ} ∧
{𝐴, ℂ} ∈
⟨𝐴, ℂ⟩)
→ ¬ ⟨𝐴,
ℂ⟩ ∈ ℂ) |
17 | 9, 14, 16 | sylancr 588 |
. . . . 5
⊢ (𝐴 ∈ V → ¬
⟨𝐴, ℂ⟩
∈ ℂ) |
18 | | opprc1 4898 |
. . . . . 6
⊢ (¬
𝐴 ∈ V →
⟨𝐴, ℂ⟩ =
∅) |
19 | | 0ncn 11128 |
. . . . . . 7
⊢ ¬
∅ ∈ ℂ |
20 | | eleq1 2822 |
. . . . . . 7
⊢
(⟨𝐴,
ℂ⟩ = ∅ → (⟨𝐴, ℂ⟩ ∈ ℂ ↔
∅ ∈ ℂ)) |
21 | 19, 20 | mtbiri 327 |
. . . . . 6
⊢
(⟨𝐴,
ℂ⟩ = ∅ → ¬ ⟨𝐴, ℂ⟩ ∈
ℂ) |
22 | 18, 21 | syl 17 |
. . . . 5
⊢ (¬
𝐴 ∈ V → ¬
⟨𝐴, ℂ⟩
∈ ℂ) |
23 | 17, 22 | pm2.61i 182 |
. . . 4
⊢ ¬
⟨𝐴, ℂ⟩
∈ ℂ |
24 | | eqcom 2740 |
. . . . . 6
⊢
((+∞ei‘𝐴) = ⟨𝐴, ℂ⟩ ↔ ⟨𝐴, ℂ⟩ =
(+∞ei‘𝐴)) |
25 | 24 | biimpi 215 |
. . . . 5
⊢
((+∞ei‘𝐴) = ⟨𝐴, ℂ⟩ → ⟨𝐴, ℂ⟩ =
(+∞ei‘𝐴)) |
26 | 25 | eleq1d 2819 |
. . . 4
⊢
((+∞ei‘𝐴) = ⟨𝐴, ℂ⟩ → (⟨𝐴, ℂ⟩ ∈ ℂ
↔ (+∞ei‘𝐴) ∈ ℂ)) |
27 | 23, 26 | mtbii 326 |
. . 3
⊢
((+∞ei‘𝐴) = ⟨𝐴, ℂ⟩ → ¬
(+∞ei‘𝐴) ∈ ℂ) |
28 | 7, 27 | syl 17 |
. 2
⊢ (𝐴 ∈ dom
+∞ei → ¬ (+∞ei‘𝐴) ∈
ℂ) |
29 | | ndmfv 6927 |
. . . 4
⊢ (¬
𝐴 ∈ dom
+∞ei → (+∞ei‘𝐴) = ∅) |
30 | 29 | eleq1d 2819 |
. . 3
⊢ (¬
𝐴 ∈ dom
+∞ei → ((+∞ei‘𝐴) ∈ ℂ ↔ ∅ ∈
ℂ)) |
31 | 19, 30 | mtbiri 327 |
. 2
⊢ (¬
𝐴 ∈ dom
+∞ei → ¬ (+∞ei‘𝐴) ∈
ℂ) |
32 | 28, 31 | pm2.61i 182 |
1
⊢ ¬
(+∞ei‘𝐴) ∈ ℂ |