Step | Hyp | Ref
| Expression |
1 | | bj-inftyexpidisj 32274 |
. . . 4
⊢ ¬
(inftyexpi ‘𝑦) ∈
ℂ |
2 | 1 | nex 1722 |
. . 3
⊢ ¬
∃𝑦(inftyexpi
‘𝑦) ∈
ℂ |
3 | | elin 3758 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∩
ℂ∞) ↔ (𝑥 ∈ ℂ ∧ 𝑥 ∈
ℂ∞)) |
4 | | df-bj-inftyexpi 32271 |
. . . . . . . . . . 11
⊢ inftyexpi
= (𝑧 ∈ (-π(,]π)
↦ 〈𝑧,
ℂ〉) |
5 | 4 | funmpt2 5841 |
. . . . . . . . . 10
⊢ Fun
inftyexpi |
6 | | elrnrexdm 6271 |
. . . . . . . . . 10
⊢ (Fun
inftyexpi → (𝑥 ∈
ran inftyexpi → ∃𝑦 ∈ dom inftyexpi 𝑥 = (inftyexpi ‘𝑦))) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran inftyexpi →
∃𝑦 ∈ dom
inftyexpi 𝑥 = (inftyexpi
‘𝑦)) |
8 | | rexex 2985 |
. . . . . . . . 9
⊢
(∃𝑦 ∈ dom
inftyexpi 𝑥 = (inftyexpi
‘𝑦) →
∃𝑦 𝑥 = (inftyexpi ‘𝑦)) |
9 | 7, 8 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ran inftyexpi →
∃𝑦 𝑥 = (inftyexpi ‘𝑦)) |
10 | | df-bj-ccinfty 32276 |
. . . . . . . 8
⊢
ℂ∞ = ran inftyexpi |
11 | 9, 10 | eleq2s 2706 |
. . . . . . 7
⊢ (𝑥 ∈
ℂ∞ → ∃𝑦 𝑥 = (inftyexpi ‘𝑦)) |
12 | 11 | anim2i 591 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ∈
ℂ∞) → (𝑥 ∈ ℂ ∧ ∃𝑦 𝑥 = (inftyexpi ‘𝑦))) |
13 | 3, 12 | sylbi 206 |
. . . . 5
⊢ (𝑥 ∈ (ℂ ∩
ℂ∞) → (𝑥 ∈ ℂ ∧ ∃𝑦 𝑥 = (inftyexpi ‘𝑦))) |
14 | | ancom 465 |
. . . . . 6
⊢ ((𝑥 ∈ ℂ ∧
∃𝑦 𝑥 = (inftyexpi ‘𝑦)) ↔ (∃𝑦 𝑥 = (inftyexpi ‘𝑦) ∧ 𝑥 ∈ ℂ)) |
15 | | exancom 1774 |
. . . . . . 7
⊢
(∃𝑦(𝑥 ∈ ℂ ∧ 𝑥 = (inftyexpi ‘𝑦)) ↔ ∃𝑦(𝑥 = (inftyexpi ‘𝑦) ∧ 𝑥 ∈ ℂ)) |
16 | | 19.41v 1901 |
. . . . . . 7
⊢
(∃𝑦(𝑥 = (inftyexpi ‘𝑦) ∧ 𝑥 ∈ ℂ) ↔ (∃𝑦 𝑥 = (inftyexpi ‘𝑦) ∧ 𝑥 ∈ ℂ)) |
17 | 15, 16 | bitri 263 |
. . . . . 6
⊢
(∃𝑦(𝑥 ∈ ℂ ∧ 𝑥 = (inftyexpi ‘𝑦)) ↔ (∃𝑦 𝑥 = (inftyexpi ‘𝑦) ∧ 𝑥 ∈ ℂ)) |
18 | 14, 17 | sylbb2 227 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧
∃𝑦 𝑥 = (inftyexpi ‘𝑦)) → ∃𝑦(𝑥 ∈ ℂ ∧ 𝑥 = (inftyexpi ‘𝑦))) |
19 | 13, 18 | syl 17 |
. . . 4
⊢ (𝑥 ∈ (ℂ ∩
ℂ∞) → ∃𝑦(𝑥 ∈ ℂ ∧ 𝑥 = (inftyexpi ‘𝑦))) |
20 | | eleq1 2676 |
. . . . . 6
⊢ (𝑥 = (inftyexpi ‘𝑦) → (𝑥 ∈ ℂ ↔ (inftyexpi
‘𝑦) ∈
ℂ)) |
21 | 20 | biimpac 502 |
. . . . 5
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 = (inftyexpi ‘𝑦)) → (inftyexpi
‘𝑦) ∈
ℂ) |
22 | 21 | eximi 1752 |
. . . 4
⊢
(∃𝑦(𝑥 ∈ ℂ ∧ 𝑥 = (inftyexpi ‘𝑦)) → ∃𝑦(inftyexpi ‘𝑦) ∈
ℂ) |
23 | 19, 22 | syl 17 |
. . 3
⊢ (𝑥 ∈ (ℂ ∩
ℂ∞) → ∃𝑦(inftyexpi ‘𝑦) ∈ ℂ) |
24 | 2, 23 | mto 187 |
. 2
⊢ ¬
𝑥 ∈ (ℂ ∩
ℂ∞) |
25 | 24 | bj-nel0 32128 |
1
⊢ (ℂ
∩ ℂ∞) = ∅ |