Metamath Proof Explorer


Theorem lmcnp

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014)

Ref Expression
Hypotheses lmcnp.3 φFtJP
lmcnp.4 φGJCnPKP
Assertion lmcnp φGFtKGP

Proof

Step Hyp Ref Expression
1 lmcnp.3 φFtJP
2 lmcnp.4 φGJCnPKP
3 eqid J=J
4 eqid K=K
5 3 4 cnpf GJCnPKPG:JK
6 2 5 syl φG:JK
7 cnptop1 GJCnPKPJTop
8 2 7 syl φJTop
9 toptopon2 JTopJTopOnJ
10 8 9 sylib φJTopOnJ
11 nnuz =1
12 1zzd φ1
13 10 11 12 lmbr2 φFtJPFJ𝑝𝑚PJvJPvjkjkdomFFkv
14 1 13 mpbid φFJ𝑝𝑚PJvJPvjkjkdomFFkv
15 14 simp1d φFJ𝑝𝑚
16 8 uniexd φJV
17 cnex V
18 elpm2g JVVFJ𝑝𝑚F:domFJdomF
19 16 17 18 sylancl φFJ𝑝𝑚F:domFJdomF
20 15 19 mpbid φF:domFJdomF
21 20 simpld φF:domFJ
22 fco G:JKF:domFJGF:domFK
23 6 21 22 syl2anc φGF:domFK
24 23 ffdmd φGF:domGFK
25 23 fdmd φdomGF=domF
26 20 simprd φdomF
27 25 26 eqsstrd φdomGF
28 cnptop2 GJCnPKPKTop
29 2 28 syl φKTop
30 29 uniexd φKV
31 elpm2g KVVGFK𝑝𝑚GF:domGFKdomGF
32 30 17 31 sylancl φGFK𝑝𝑚GF:domGFKdomGF
33 24 27 32 mpbir2and φGFK𝑝𝑚
34 14 simp2d φPJ
35 6 34 ffvelrnd φGPK
36 14 simp3d φvJPvjkjkdomFFkv
37 36 adantr φuKGPuvJPvjkjkdomFFkv
38 cnpimaex GJCnPKPuKGPuvJPvGvu
39 38 3expb GJCnPKPuKGPuvJPvGvu
40 2 39 sylan φuKGPuvJPvGvu
41 r19.29 vJPvjkjkdomFFkvvJPvGvuvJPvjkjkdomFFkvPvGvu
42 pm3.45 PvjkjkdomFFkvPvGvujkjkdomFFkvGvu
43 42 imp PvjkjkdomFFkvPvGvujkjkdomFFkvGvu
44 43 reximi vJPvjkjkdomFFkvPvGvuvJjkjkdomFFkvGvu
45 41 44 syl vJPvjkjkdomFFkvvJPvGvuvJjkjkdomFFkvGvu
46 6 ad3antrrr φuKGPuvJGvukdomFG:JK
47 46 ffnd φuKGPuvJGvukdomFGFnJ
48 simplrl φuKGPuvJGvukdomFvJ
49 elssuni vJvJ
50 48 49 syl φuKGPuvJGvukdomFvJ
51 fnfvima GFnJvJFkvGFkGv
52 51 3expia GFnJvJFkvGFkGv
53 47 50 52 syl2anc φuKGPuvJGvukdomFFkvGFkGv
54 21 ad2antrr φuKGPuvJGvuF:domFJ
55 fvco3 F:domFJkdomFGFk=GFk
56 54 55 sylan φuKGPuvJGvukdomFGFk=GFk
57 56 eleq1d φuKGPuvJGvukdomFGFkGvGFkGv
58 53 57 sylibrd φuKGPuvJGvukdomFFkvGFkGv
59 simplrr φuKGPuvJGvukdomFGvu
60 59 sseld φuKGPuvJGvukdomFGFkGvGFku
61 58 60 syld φuKGPuvJGvukdomFFkvGFku
62 simpr φuKGPuvJGvukdomFkdomF
63 25 ad3antrrr φuKGPuvJGvukdomFdomGF=domF
64 62 63 eleqtrrd φuKGPuvJGvukdomFkdomGF
65 61 64 jctild φuKGPuvJGvukdomFFkvkdomGFGFku
66 65 expimpd φuKGPuvJGvukdomFFkvkdomGFGFku
67 66 ralimdv φuKGPuvJGvukjkdomFFkvkjkdomGFGFku
68 67 reximdv φuKGPuvJGvujkjkdomFFkvjkjkdomGFGFku
69 68 expr φuKGPuvJGvujkjkdomFFkvjkjkdomGFGFku
70 69 impcomd φuKGPuvJjkjkdomFFkvGvujkjkdomGFGFku
71 70 rexlimdva φuKGPuvJjkjkdomFFkvGvujkjkdomGFGFku
72 45 71 syl5 φuKGPuvJPvjkjkdomFFkvvJPvGvujkjkdomGFGFku
73 37 40 72 mp2and φuKGPujkjkdomGFGFku
74 73 expr φuKGPujkjkdomGFGFku
75 74 ralrimiva φuKGPujkjkdomGFGFku
76 toptopon2 KTopKTopOnK
77 29 76 sylib φKTopOnK
78 77 11 12 lmbr2 φGFtKGPGFK𝑝𝑚GPKuKGPujkjkdomGFGFku
79 33 35 75 78 mpbir3and φGFtKGP