Metamath Proof Explorer

Theorem ellimc2

Description: Write the definition of a limit directly in terms of open sets of the topology on the complex numbers. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limccl.f ⊢φ→F:A⟶ℂ
limccl.a ⊢φ→A⊆ℂ
limccl.b ⊢φ→B∈ℂ
ellimc2.k ⊢K=TopOpen⁡ℂfld
Assertion ellimc2 ⊢φ→C∈FlimℂB↔C∈ℂ∧∀u∈KC∈u→∃w∈KB∈w∧Fw∩A∖B⊆u

Proof

Step Hyp Ref Expression
1 limccl.f ⊢φ→F:A⟶ℂ
2 limccl.a ⊢φ→A⊆ℂ
3 limccl.b ⊢φ→B∈ℂ
4 ellimc2.k ⊢K=TopOpen⁡ℂfld
5 limccl ⊢FlimℂB⊆ℂ
6 5 sseli ⊢C∈FlimℂB→C∈ℂ
7 6 pm4.71ri ⊢C∈FlimℂB↔C∈ℂ∧C∈FlimℂB
8 eqid ⊢K↾𝑡A∪B=K↾𝑡A∪B
9 eqid ⊢z∈A∪B⟼ifz=BCF⁡z=z∈A∪B⟼ifz=BCF⁡z
10 8 4 9 1 2 3 ellimc ⊢φ→C∈FlimℂB↔z∈A∪B⟼ifz=BCF⁡z∈K↾𝑡A∪BCnPK⁡B
11 10 adantr ⊢φ∧C∈ℂ→C∈FlimℂB↔z∈A∪B⟼ifz=BCF⁡z∈K↾𝑡A∪BCnPK⁡B
12 4 cnfldtopon ⊢K∈TopOn⁡ℂ
13 3 snssd ⊢φ→B⊆ℂ
14 2 13 unssd ⊢φ→A∪B⊆ℂ
15 resttopon ⊢K∈TopOn⁡ℂ∧A∪B⊆ℂ→K↾𝑡A∪B∈TopOn⁡A∪B
16 12 14 15 sylancr ⊢φ→K↾𝑡A∪B∈TopOn⁡A∪B
17 16 adantr ⊢φ∧C∈ℂ→K↾𝑡A∪B∈TopOn⁡A∪B
18 12 a1i ⊢φ∧C∈ℂ→K∈TopOn⁡ℂ
19 ssun2 ⊢B⊆A∪B
20 snssg ⊢B∈ℂ→B∈A∪B↔B⊆A∪B
21 3 20 syl ⊢φ→B∈A∪B↔B⊆A∪B
22 19 21 mpbiri ⊢φ→B∈A∪B
23 22 adantr ⊢φ∧C∈ℂ→B∈A∪B
24 elun ⊢z∈A∪B↔z∈A∨z∈B
25 velsn ⊢z∈B↔z=B
26 25 orbi2i ⊢z∈A∨z∈B↔z∈A∨z=B
27 24 26 bitri ⊢z∈A∪B↔z∈A∨z=B
28 simpllr ⊢φ∧C∈ℂ∧z∈A∨z=B∧z=B→C∈ℂ
29 pm5.61 ⊢z∈A∨z=B∧¬z=B↔z∈A∧¬z=B
30 1 ffvelcdmda ⊢φ∧z∈A→F⁡z∈ℂ
31 30 ad2ant2r ⊢φ∧C∈ℂ∧z∈A∧¬z=B→F⁡z∈ℂ
32 29 31 sylan2b ⊢φ∧C∈ℂ∧z∈A∨z=B∧¬z=B→F⁡z∈ℂ
33 32 anassrs ⊢φ∧C∈ℂ∧z∈A∨z=B∧¬z=B→F⁡z∈ℂ
34 28 33 ifclda ⊢φ∧C∈ℂ∧z∈A∨z=B→ifz=BCF⁡z∈ℂ
35 27 34 sylan2b ⊢φ∧C∈ℂ∧z∈A∪B→ifz=BCF⁡z∈ℂ
36 35 fmpttd ⊢φ∧C∈ℂ→z∈A∪B⟼ifz=BCF⁡z:A∪B⟶ℂ
37 iscnp ⊢K↾𝑡A∪B∈TopOn⁡A∪B∧K∈TopOn⁡ℂ∧B∈A∪B→z∈A∪B⟼ifz=BCF⁡z∈K↾𝑡A∪BCnPK⁡B↔z∈A∪B⟼ifz=BCF⁡z:A∪B⟶ℂ∧∀u∈Kz∈A∪B⟼ifz=BCF⁡z⁡B∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u
38 37 baibd ⊢K↾𝑡A∪B∈TopOn⁡A∪B∧K∈TopOn⁡ℂ∧B∈A∪B∧z∈A∪B⟼ifz=BCF⁡z:A∪B⟶ℂ→z∈A∪B⟼ifz=BCF⁡z∈K↾𝑡A∪BCnPK⁡B↔∀u∈Kz∈A∪B⟼ifz=BCF⁡z⁡B∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u
39 17 18 23 36 38 syl31anc ⊢φ∧C∈ℂ→z∈A∪B⟼ifz=BCF⁡z∈K↾𝑡A∪BCnPK⁡B↔∀u∈Kz∈A∪B⟼ifz=BCF⁡z⁡B∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u
40 iftrue ⊢z=B→ifz=BCF⁡z=C
41 40 9 fvmptg ⊢B∈A∪B∧C∈ℂ→z∈A∪B⟼ifz=BCF⁡z⁡B=C
42 22 41 sylan ⊢φ∧C∈ℂ→z∈A∪B⟼ifz=BCF⁡z⁡B=C
43 42 eleq1d ⊢φ∧C∈ℂ→z∈A∪B⟼ifz=BCF⁡z⁡B∈u↔C∈u
44 43 imbi1d ⊢φ∧C∈ℂ→z∈A∪B⟼ifz=BCF⁡z⁡B∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔C∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u
45 44 adantr ⊢φ∧C∈ℂ∧u∈K→z∈A∪B⟼ifz=BCF⁡z⁡B∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔C∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u
46 4 cnfldtop ⊢K∈Top
47 cnex ⊢ℂ∈V
48 47 ssex ⊢A∪B⊆ℂ→A∪B∈V
49 14 48 syl ⊢φ→A∪B∈V
50 49 ad2antrr ⊢φ∧C∈ℂ∧u∈K∧C∈u→A∪B∈V
51 restval ⊢K∈Top∧A∪B∈V→K↾𝑡A∪B=ran⁡w∈K⟼w∩A∪B
52 46 50 51 sylancr ⊢φ∧C∈ℂ∧u∈K∧C∈u→K↾𝑡A∪B=ran⁡w∈K⟼w∩A∪B
53 52 rexeqdv ⊢φ∧C∈ℂ∧u∈K∧C∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔∃v∈ran⁡w∈K⟼w∩A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u
54 vex ⊢w∈V
55 54 inex1 ⊢w∩A∪B∈V
56 55 rgenw ⊢∀w∈Kw∩A∪B∈V
57 eqid ⊢w∈K⟼w∩A∪B=w∈K⟼w∩A∪B
58 eleq2 ⊢v=w∩A∪B→B∈v↔B∈w∩A∪B
59 imaeq2 ⊢v=w∩A∪B→z∈A∪B⟼ifz=BCF⁡zv=z∈A∪B⟼ifz=BCF⁡zw∩A∪B
60 59 sseq1d ⊢v=w∩A∪B→z∈A∪B⟼ifz=BCF⁡zv⊆u↔z∈A∪B⟼ifz=BCF⁡zw∩A∪B⊆u
61 58 60 anbi12d ⊢v=w∩A∪B→B∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔B∈w∩A∪B∧z∈A∪B⟼ifz=BCF⁡zw∩A∪B⊆u
62 57 61 rexrnmptw ⊢∀w∈Kw∩A∪B∈V→∃v∈ran⁡w∈K⟼w∩A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔∃w∈KB∈w∩A∪B∧z∈A∪B⟼ifz=BCF⁡zw∩A∪B⊆u
63 56 62 mp1i ⊢φ∧C∈ℂ∧u∈K∧C∈u→∃v∈ran⁡w∈K⟼w∩A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔∃w∈KB∈w∩A∪B∧z∈A∪B⟼ifz=BCF⁡zw∩A∪B⊆u
64 22 ad3antrrr ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→B∈A∪B
65 elin ⊢B∈w∩A∪B↔B∈w∧B∈A∪B
66 65 rbaib ⊢B∈A∪B→B∈w∩A∪B↔B∈w
67 64 66 syl ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→B∈w∩A∪B↔B∈w
68 simpllr ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→C∈ℂ
69 fvex ⊢F⁡z∈V
70 ifexg ⊢C∈ℂ∧F⁡z∈V→ifz=BCF⁡z∈V
71 68 69 70 sylancl ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→ifz=BCF⁡z∈V
72 71 ralrimivw ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→∀z∈w∩A∪Bifz=BCF⁡z∈V
73 eqid ⊢z∈w∩A∪B⟼ifz=BCF⁡z=z∈w∩A∪B⟼ifz=BCF⁡z
74 73 fnmpt ⊢∀z∈w∩A∪Bifz=BCF⁡z∈V→z∈w∩A∪B⟼ifz=BCF⁡zFnw∩A∪B
75 73 fmpt ⊢∀z∈w∩A∪Bifz=BCF⁡z∈u↔z∈w∩A∪B⟼ifz=BCF⁡z:w∩A∪B⟶u
76 df-f ⊢z∈w∩A∪B⟼ifz=BCF⁡z:w∩A∪B⟶u↔z∈w∩A∪B⟼ifz=BCF⁡zFnw∩A∪B∧ran⁡z∈w∩A∪B⟼ifz=BCF⁡z⊆u
77 75 76 bitri ⊢∀z∈w∩A∪Bifz=BCF⁡z∈u↔z∈w∩A∪B⟼ifz=BCF⁡zFnw∩A∪B∧ran⁡z∈w∩A∪B⟼ifz=BCF⁡z⊆u
78 77 baib ⊢z∈w∩A∪B⟼ifz=BCF⁡zFnw∩A∪B→∀z∈w∩A∪Bifz=BCF⁡z∈u↔ran⁡z∈w∩A∪B⟼ifz=BCF⁡z⊆u
79 72 74 78 3syl ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→∀z∈w∩A∪Bifz=BCF⁡z∈u↔ran⁡z∈w∩A∪B⟼ifz=BCF⁡z⊆u
80 simplrr ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→C∈u
81 elinel2 ⊢z∈w∩B→z∈B
82 25 40 sylbi ⊢z∈B→ifz=BCF⁡z=C
83 82 eleq1d ⊢z∈B→ifz=BCF⁡z∈u↔C∈u
84 81 83 syl ⊢z∈w∩B→ifz=BCF⁡z∈u↔C∈u
85 80 84 syl5ibrcom ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→z∈w∩B→ifz=BCF⁡z∈u
86 85 ralrimiv ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→∀z∈w∩Bifz=BCF⁡z∈u
87 undif1 ⊢A∖B∪B=A∪B
88 87 ineq2i ⊢w∩A∖B∪B=w∩A∪B
89 indi ⊢w∩A∖B∪B=w∩A∖B∪w∩B
90 88 89 eqtr3i ⊢w∩A∪B=w∩A∖B∪w∩B
91 90 raleqi ⊢∀z∈w∩A∪Bifz=BCF⁡z∈u↔∀z∈w∩A∖B∪w∩Bifz=BCF⁡z∈u
92 ralunb ⊢∀z∈w∩A∖B∪w∩Bifz=BCF⁡z∈u↔∀z∈w∩A∖Bifz=BCF⁡z∈u∧∀z∈w∩Bifz=BCF⁡z∈u
93 91 92 bitri ⊢∀z∈w∩A∪Bifz=BCF⁡z∈u↔∀z∈w∩A∖Bifz=BCF⁡z∈u∧∀z∈w∩Bifz=BCF⁡z∈u
94 93 rbaib ⊢∀z∈w∩Bifz=BCF⁡z∈u→∀z∈w∩A∪Bifz=BCF⁡z∈u↔∀z∈w∩A∖Bifz=BCF⁡z∈u
95 86 94 syl ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→∀z∈w∩A∪Bifz=BCF⁡z∈u↔∀z∈w∩A∖Bifz=BCF⁡z∈u
96 79 95 bitr3d ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→ran⁡z∈w∩A∪B⟼ifz=BCF⁡z⊆u↔∀z∈w∩A∖Bifz=BCF⁡z∈u
97 elinel2 ⊢z∈w∩A∖B→z∈A∖B
98 eldifsni ⊢z∈A∖B→z≠B
99 ifnefalse ⊢z≠B→ifz=BCF⁡z=F⁡z
100 98 99 syl ⊢z∈A∖B→ifz=BCF⁡z=F⁡z
101 100 eleq1d ⊢z∈A∖B→ifz=BCF⁡z∈u↔F⁡z∈u
102 97 101 syl ⊢z∈w∩A∖B→ifz=BCF⁡z∈u↔F⁡z∈u
103 102 ralbiia ⊢∀z∈w∩A∖Bifz=BCF⁡z∈u↔∀z∈w∩A∖BF⁡z∈u
104 96 103 bitrdi ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→ran⁡z∈w∩A∪B⟼ifz=BCF⁡z⊆u↔∀z∈w∩A∖BF⁡z∈u
105 df-ima ⊢z∈A∪B⟼ifz=BCF⁡zw∩A∪B=ran⁡z∈A∪B⟼ifz=BCF⁡z↾w∩A∪B
106 inss2 ⊢w∩A∪B⊆A∪B
107 resmpt ⊢w∩A∪B⊆A∪B→z∈A∪B⟼ifz=BCF⁡z↾w∩A∪B=z∈w∩A∪B⟼ifz=BCF⁡z
108 106 107 mp1i ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→z∈A∪B⟼ifz=BCF⁡z↾w∩A∪B=z∈w∩A∪B⟼ifz=BCF⁡z
109 108 rneqd ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→ran⁡z∈A∪B⟼ifz=BCF⁡z↾w∩A∪B=ran⁡z∈w∩A∪B⟼ifz=BCF⁡z
110 105 109 eqtrid ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→z∈A∪B⟼ifz=BCF⁡zw∩A∪B=ran⁡z∈w∩A∪B⟼ifz=BCF⁡z
111 110 sseq1d ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→z∈A∪B⟼ifz=BCF⁡zw∩A∪B⊆u↔ran⁡z∈w∩A∪B⟼ifz=BCF⁡z⊆u
112 1 ad3antrrr ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→F:A⟶ℂ
113 112 ffund ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→Fun⁡F
114 inss2 ⊢w∩A∖B⊆A∖B
115 difss ⊢A∖B⊆A
116 114 115 sstri ⊢w∩A∖B⊆A
117 112 fdmd ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→dom⁡F=A
118 116 117 sseqtrrid ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→w∩A∖B⊆dom⁡F
119 funimass4 ⊢Fun⁡F∧w∩A∖B⊆dom⁡F→Fw∩A∖B⊆u↔∀z∈w∩A∖BF⁡z∈u
120 113 118 119 syl2anc ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→Fw∩A∖B⊆u↔∀z∈w∩A∖BF⁡z∈u
121 104 111 120 3bitr4d ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→z∈A∪B⟼ifz=BCF⁡zw∩A∪B⊆u↔Fw∩A∖B⊆u
122 67 121 anbi12d ⊢φ∧C∈ℂ∧u∈K∧C∈u∧w∈K→B∈w∩A∪B∧z∈A∪B⟼ifz=BCF⁡zw∩A∪B⊆u↔B∈w∧Fw∩A∖B⊆u
123 122 rexbidva ⊢φ∧C∈ℂ∧u∈K∧C∈u→∃w∈KB∈w∩A∪B∧z∈A∪B⟼ifz=BCF⁡zw∩A∪B⊆u↔∃w∈KB∈w∧Fw∩A∖B⊆u
124 53 63 123 3bitrd ⊢φ∧C∈ℂ∧u∈K∧C∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔∃w∈KB∈w∧Fw∩A∖B⊆u
125 124 anassrs ⊢φ∧C∈ℂ∧u∈K∧C∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔∃w∈KB∈w∧Fw∩A∖B⊆u
126 125 pm5.74da ⊢φ∧C∈ℂ∧u∈K→C∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔C∈u→∃w∈KB∈w∧Fw∩A∖B⊆u
127 45 126 bitrd ⊢φ∧C∈ℂ∧u∈K→z∈A∪B⟼ifz=BCF⁡z⁡B∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔C∈u→∃w∈KB∈w∧Fw∩A∖B⊆u
128 127 ralbidva ⊢φ∧C∈ℂ→∀u∈Kz∈A∪B⟼ifz=BCF⁡z⁡B∈u→∃v∈K↾𝑡A∪BB∈v∧z∈A∪B⟼ifz=BCF⁡zv⊆u↔∀u∈KC∈u→∃w∈KB∈w∧Fw∩A∖B⊆u
129 11 39 128 3bitrd ⊢φ∧C∈ℂ→C∈FlimℂB↔∀u∈KC∈u→∃w∈KB∈w∧Fw∩A∖B⊆u
130 129 pm5.32da ⊢φ→C∈ℂ∧C∈FlimℂB↔C∈ℂ∧∀u∈KC∈u→∃w∈KB∈w∧Fw∩A∖B⊆u
131 7 130 bitrid ⊢φ→C∈FlimℂB↔C∈ℂ∧∀u∈KC∈u→∃w∈KB∈w∧Fw∩A∖B⊆u