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 
|- ( ph -> F ( ~~>t ` J ) P )
lmcnp.4 
|- ( ph -> G e. ( ( J CnP K ) ` P ) )
Assertion lmcnp 
|- ( ph -> ( G o. F ) ( ~~>t ` K ) ( G ` P ) )

Proof

Step Hyp Ref Expression
1 lmcnp.3 
 |-  ( ph -> F ( ~~>t ` J ) P )
2 lmcnp.4 
 |-  ( ph -> G e. ( ( J CnP K ) ` P ) )
3 eqid 
 |-  U. J = U. J
4 eqid 
 |-  U. K = U. K
5 3 4 cnpf 
 |-  ( G e. ( ( J CnP K ) ` P ) -> G : U. J --> U. K )
6 2 5 syl 
 |-  ( ph -> G : U. J --> U. K )
7 cnptop1 
 |-  ( G e. ( ( J CnP K ) ` P ) -> J e. Top )
8 2 7 syl 
 |-  ( ph -> J e. Top )
9 toptopon2 
 |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )
10 8 9 sylib 
 |-  ( ph -> J e. ( TopOn ` U. J ) )
11 nnuz 
 |-  NN = ( ZZ>= ` 1 )
12 1zzd 
 |-  ( ph -> 1 e. ZZ )
13 10 11 12 lmbr2 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( U. J ^pm CC ) /\ P e. U. J /\ A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) ) ) )
14 1 13 mpbid 
 |-  ( ph -> ( F e. ( U. J ^pm CC ) /\ P e. U. J /\ A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) ) )
15 14 simp1d 
 |-  ( ph -> F e. ( U. J ^pm CC ) )
16 8 uniexd 
 |-  ( ph -> U. J e. _V )
17 cnex 
 |-  CC e. _V
18 elpm2g 
 |-  ( ( U. J e. _V /\ CC e. _V ) -> ( F e. ( U. J ^pm CC ) <-> ( F : dom F --> U. J /\ dom F C_ CC ) ) )
19 16 17 18 sylancl 
 |-  ( ph -> ( F e. ( U. J ^pm CC ) <-> ( F : dom F --> U. J /\ dom F C_ CC ) ) )
20 15 19 mpbid 
 |-  ( ph -> ( F : dom F --> U. J /\ dom F C_ CC ) )
21 20 simpld 
 |-  ( ph -> F : dom F --> U. J )
22 fco 
 |-  ( ( G : U. J --> U. K /\ F : dom F --> U. J ) -> ( G o. F ) : dom F --> U. K )
23 6 21 22 syl2anc 
 |-  ( ph -> ( G o. F ) : dom F --> U. K )
24 23 ffdmd 
 |-  ( ph -> ( G o. F ) : dom ( G o. F ) --> U. K )
25 23 fdmd 
 |-  ( ph -> dom ( G o. F ) = dom F )
26 20 simprd 
 |-  ( ph -> dom F C_ CC )
27 25 26 eqsstrd 
 |-  ( ph -> dom ( G o. F ) C_ CC )
28 cnptop2 
 |-  ( G e. ( ( J CnP K ) ` P ) -> K e. Top )
29 2 28 syl 
 |-  ( ph -> K e. Top )
30 29 uniexd 
 |-  ( ph -> U. K e. _V )
31 elpm2g 
 |-  ( ( U. K e. _V /\ CC e. _V ) -> ( ( G o. F ) e. ( U. K ^pm CC ) <-> ( ( G o. F ) : dom ( G o. F ) --> U. K /\ dom ( G o. F ) C_ CC ) ) )
32 30 17 31 sylancl 
 |-  ( ph -> ( ( G o. F ) e. ( U. K ^pm CC ) <-> ( ( G o. F ) : dom ( G o. F ) --> U. K /\ dom ( G o. F ) C_ CC ) ) )
33 24 27 32 mpbir2and 
 |-  ( ph -> ( G o. F ) e. ( U. K ^pm CC ) )
34 14 simp2d 
 |-  ( ph -> P e. U. J )
35 6 34 ffvelcdmd 
 |-  ( ph -> ( G ` P ) e. U. K )
36 14 simp3d 
 |-  ( ph -> A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) )
37 36 adantr 
 |-  ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) )
38 cnpimaex 
 |-  ( ( G e. ( ( J CnP K ) ` P ) /\ u e. K /\ ( G ` P ) e. u ) -> E. v e. J ( P e. v /\ ( G " v ) C_ u ) )
39 38 3expb 
 |-  ( ( G e. ( ( J CnP K ) ` P ) /\ ( u e. K /\ ( G ` P ) e. u ) ) -> E. v e. J ( P e. v /\ ( G " v ) C_ u ) )
40 2 39 sylan 
 |-  ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> E. v e. J ( P e. v /\ ( G " v ) C_ u ) )
41 r19.29 
 |-  ( ( A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ E. v e. J ( P e. v /\ ( G " v ) C_ u ) ) -> E. v e. J ( ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ ( P e. v /\ ( G " v ) C_ u ) ) )
42 pm3.45 
 |-  ( ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) -> ( ( P e. v /\ ( G " v ) C_ u ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) ) )
43 42 imp 
 |-  ( ( ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ ( P e. v /\ ( G " v ) C_ u ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) )
44 43 reximi 
 |-  ( E. v e. J ( ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ ( P e. v /\ ( G " v ) C_ u ) ) -> E. v e. J ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) )
45 41 44 syl 
 |-  ( ( A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ E. v e. J ( P e. v /\ ( G " v ) C_ u ) ) -> E. v e. J ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) )
46 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> G : U. J --> U. K )
47 46 ffnd 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> G Fn U. J )
48 simplrl 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> v e. J )
49 elssuni 
 |-  ( v e. J -> v C_ U. J )
50 48 49 syl 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> v C_ U. J )
51 fnfvima 
 |-  ( ( G Fn U. J /\ v C_ U. J /\ ( F ` k ) e. v ) -> ( G ` ( F ` k ) ) e. ( G " v ) )
52 51 3expia 
 |-  ( ( G Fn U. J /\ v C_ U. J ) -> ( ( F ` k ) e. v -> ( G ` ( F ` k ) ) e. ( G " v ) ) )
53 47 50 52 syl2anc 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( F ` k ) e. v -> ( G ` ( F ` k ) ) e. ( G " v ) ) )
54 21 ad2antrr 
 |-  ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) -> F : dom F --> U. J )
55 fvco3 
 |-  ( ( F : dom F --> U. J /\ k e. dom F ) -> ( ( G o. F ) ` k ) = ( G ` ( F ` k ) ) )
56 54 55 sylan 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( G o. F ) ` k ) = ( G ` ( F ` k ) ) )
57 56 eleq1d 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( ( G o. F ) ` k ) e. ( G " v ) <-> ( G ` ( F ` k ) ) e. ( G " v ) ) )
58 53 57 sylibrd 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( F ` k ) e. v -> ( ( G o. F ) ` k ) e. ( G " v ) ) )
59 simplrr 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( G " v ) C_ u )
60 59 sseld 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( ( G o. F ) ` k ) e. ( G " v ) -> ( ( G o. F ) ` k ) e. u ) )
61 58 60 syld 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( F ` k ) e. v -> ( ( G o. F ) ` k ) e. u ) )
62 simpr 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> k e. dom F )
63 25 ad3antrrr 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> dom ( G o. F ) = dom F )
64 62 63 eleqtrrd 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> k e. dom ( G o. F ) )
65 61 64 jctild 
 |-  ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( F ` k ) e. v -> ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
66 65 expimpd 
 |-  ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) -> ( ( k e. dom F /\ ( F ` k ) e. v ) -> ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
67 66 ralimdv 
 |-  ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) -> A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
68 67 reximdv 
 |-  ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
69 68 expr 
 |-  ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ v e. J ) -> ( ( G " v ) C_ u -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) ) )
70 69 impcomd 
 |-  ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ v e. J ) -> ( ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
71 70 rexlimdva 
 |-  ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> ( E. v e. J ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
72 45 71 syl5 
 |-  ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> ( ( A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ E. v e. J ( P e. v /\ ( G " v ) C_ u ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
73 37 40 72 mp2and 
 |-  ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) )
74 73 expr 
 |-  ( ( ph /\ u e. K ) -> ( ( G ` P ) e. u -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
75 74 ralrimiva 
 |-  ( ph -> A. u e. K ( ( G ` P ) e. u -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
76 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
77 29 76 sylib 
 |-  ( ph -> K e. ( TopOn ` U. K ) )
78 77 11 12 lmbr2 
 |-  ( ph -> ( ( G o. F ) ( ~~>t ` K ) ( G ` P ) <-> ( ( G o. F ) e. ( U. K ^pm CC ) /\ ( G ` P ) e. U. K /\ A. u e. K ( ( G ` P ) e. u -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) ) ) )
79 33 35 75 78 mpbir3and 
 |-  ( ph -> ( G o. F ) ( ~~>t ` K ) ( G ` P ) )