Step | Hyp | Ref
| Expression |
1 | | opeq1 4340 |
. . . . 5
⊢ (𝑥 = 𝐴 → 〈𝑥, ℂ〉 = 〈𝐴, ℂ〉) |
2 | | df-bj-inftyexpi 32271 |
. . . . 5
⊢ inftyexpi
= (𝑥 ∈ (-π(,]π)
↦ 〈𝑥,
ℂ〉) |
3 | | opex 4859 |
. . . . 5
⊢
〈𝐴,
ℂ〉 ∈ V |
4 | 1, 2, 3 | fvmpt 6191 |
. . . 4
⊢ (𝐴 ∈ (-π(,]π) →
(inftyexpi ‘𝐴) =
〈𝐴,
ℂ〉) |
5 | | opex 4859 |
. . . . 5
⊢
〈𝑥,
ℂ〉 ∈ V |
6 | 5, 2 | dmmpti 5936 |
. . . 4
⊢ dom
inftyexpi = (-π(,]π) |
7 | 4, 6 | eleq2s 2706 |
. . 3
⊢ (𝐴 ∈ dom inftyexpi →
(inftyexpi ‘𝐴) =
〈𝐴,
ℂ〉) |
8 | | cnex 9896 |
. . . . . . 7
⊢ ℂ
∈ V |
9 | 8 | prid2 4242 |
. . . . . 6
⊢ ℂ
∈ {𝐴,
ℂ} |
10 | | eqid 2610 |
. . . . . . . 8
⊢ {𝐴, ℂ} = {𝐴, ℂ} |
11 | 10 | olci 405 |
. . . . . . 7
⊢ ({𝐴, ℂ} = {𝐴} ∨ {𝐴, ℂ} = {𝐴, ℂ}) |
12 | | elopg 4861 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ ℂ ∈
V) → ({𝐴, ℂ}
∈ 〈𝐴,
ℂ〉 ↔ ({𝐴,
ℂ} = {𝐴} ∨ {𝐴, ℂ} = {𝐴, ℂ}))) |
13 | 8, 12 | mpan2 703 |
. . . . . . 7
⊢ (𝐴 ∈ V → ({𝐴, ℂ} ∈ 〈𝐴, ℂ〉 ↔ ({𝐴, ℂ} = {𝐴} ∨ {𝐴, ℂ} = {𝐴, ℂ}))) |
14 | 11, 13 | mpbiri 247 |
. . . . . 6
⊢ (𝐴 ∈ V → {𝐴, ℂ} ∈ 〈𝐴,
ℂ〉) |
15 | | en3lp 8396 |
. . . . . . 7
⊢ ¬
(ℂ ∈ {𝐴,
ℂ} ∧ {𝐴, ℂ}
∈ 〈𝐴,
ℂ〉 ∧ 〈𝐴, ℂ〉 ∈
ℂ) |
16 | 15 | bj-imn3ani 31745 |
. . . . . 6
⊢ ((ℂ
∈ {𝐴, ℂ} ∧
{𝐴, ℂ} ∈
〈𝐴, ℂ〉)
→ ¬ 〈𝐴,
ℂ〉 ∈ ℂ) |
17 | 9, 14, 16 | sylancr 694 |
. . . . 5
⊢ (𝐴 ∈ V → ¬
〈𝐴, ℂ〉
∈ ℂ) |
18 | | opprc1 4363 |
. . . . . 6
⊢ (¬
𝐴 ∈ V →
〈𝐴, ℂ〉 =
∅) |
19 | | 0ncn 9833 |
. . . . . . 7
⊢ ¬
∅ ∈ ℂ |
20 | | eleq1 2676 |
. . . . . . 7
⊢
(〈𝐴,
ℂ〉 = ∅ → (〈𝐴, ℂ〉 ∈ ℂ ↔
∅ ∈ ℂ)) |
21 | 19, 20 | mtbiri 316 |
. . . . . 6
⊢
(〈𝐴,
ℂ〉 = ∅ → ¬ 〈𝐴, ℂ〉 ∈
ℂ) |
22 | 18, 21 | syl 17 |
. . . . 5
⊢ (¬
𝐴 ∈ V → ¬
〈𝐴, ℂ〉
∈ ℂ) |
23 | 17, 22 | pm2.61i 175 |
. . . 4
⊢ ¬
〈𝐴, ℂ〉
∈ ℂ |
24 | | eqcom 2617 |
. . . . . 6
⊢
((inftyexpi ‘𝐴) = 〈𝐴, ℂ〉 ↔ 〈𝐴, ℂ〉 = (inftyexpi
‘𝐴)) |
25 | 24 | biimpi 205 |
. . . . 5
⊢
((inftyexpi ‘𝐴) = 〈𝐴, ℂ〉 → 〈𝐴, ℂ〉 = (inftyexpi
‘𝐴)) |
26 | 25 | eleq1d 2672 |
. . . 4
⊢
((inftyexpi ‘𝐴) = 〈𝐴, ℂ〉 → (〈𝐴, ℂ〉 ∈ ℂ
↔ (inftyexpi ‘𝐴)
∈ ℂ)) |
27 | 23, 26 | mtbii 315 |
. . 3
⊢
((inftyexpi ‘𝐴) = 〈𝐴, ℂ〉 → ¬ (inftyexpi
‘𝐴) ∈
ℂ) |
28 | 7, 27 | syl 17 |
. 2
⊢ (𝐴 ∈ dom inftyexpi →
¬ (inftyexpi ‘𝐴)
∈ ℂ) |
29 | | ndmfv 6128 |
. . . 4
⊢ (¬
𝐴 ∈ dom inftyexpi
→ (inftyexpi ‘𝐴)
= ∅) |
30 | 29 | eleq1d 2672 |
. . 3
⊢ (¬
𝐴 ∈ dom inftyexpi
→ ((inftyexpi ‘𝐴) ∈ ℂ ↔ ∅ ∈
ℂ)) |
31 | 19, 30 | mtbiri 316 |
. 2
⊢ (¬
𝐴 ∈ dom inftyexpi
→ ¬ (inftyexpi ‘𝐴) ∈ ℂ) |
32 | 28, 31 | pm2.61i 175 |
1
⊢ ¬
(inftyexpi ‘𝐴) ∈
ℂ |