Metamath Proof Explorer


Theorem lmlim

Description: Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on CC on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017)

Ref Expression
Hypotheses lmlim.j J TopOn Y
lmlim.f φ F : X
lmlim.p φ P X
lmlim.t J 𝑡 X = TopOpen fld 𝑡 X
lmlim.x X
Assertion lmlim φ F t J P F P

Proof

Step Hyp Ref Expression
1 lmlim.j J TopOn Y
2 lmlim.f φ F : X
3 lmlim.p φ P X
4 lmlim.t J 𝑡 X = TopOpen fld 𝑡 X
5 lmlim.x X
6 eqid J 𝑡 X = J 𝑡 X
7 nnuz = 1
8 cnex V
9 8 a1i φ V
10 5 a1i φ X
11 9 10 ssexd φ X V
12 1 topontopi J Top
13 12 a1i φ J Top
14 1z 1
15 14 a1i φ 1
16 6 7 11 13 3 15 2 lmss φ F t J P F t J 𝑡 X P
17 4 fveq2i t J 𝑡 X = t TopOpen fld 𝑡 X
18 17 breqi F t J 𝑡 X P F t TopOpen fld 𝑡 X P
19 18 a1i φ F t J 𝑡 X P F t TopOpen fld 𝑡 X P
20 eqid TopOpen fld 𝑡 X = TopOpen fld 𝑡 X
21 eqid TopOpen fld = TopOpen fld
22 21 cnfldtop TopOpen fld Top
23 22 a1i φ TopOpen fld Top
24 20 7 11 23 3 15 2 lmss φ F t TopOpen fld P F t TopOpen fld 𝑡 X P
25 fss F : X X F :
26 2 5 25 sylancl φ F :
27 21 7 lmclimf 1 F : F t TopOpen fld P F P
28 14 26 27 sylancr φ F t TopOpen fld P F P
29 24 28 bitr3d φ F t TopOpen fld 𝑡 X P F P
30 16 19 29 3bitrd φ F t J P F P