This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmcn2

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

Ref Expression
Hypotheses txlm.z 
|- Z = ( ZZ>= ` M )
txlm.m 
|- ( ph -> M e. ZZ )
txlm.j 
|- ( ph -> J e. ( TopOn ` X ) )
txlm.k 
|- ( ph -> K e. ( TopOn ` Y ) )
txlm.f 
|- ( ph -> F : Z --> X )
txlm.g 
|- ( ph -> G : Z --> Y )
lmcn2.fl 
|- ( ph -> F ( ~~>t ` J ) R )
lmcn2.gl 
|- ( ph -> G ( ~~>t ` K ) S )
lmcn2.o 
|- ( ph -> O e. ( ( J tX K ) Cn N ) )
lmcn2.h 
|- H = ( n e. Z |-> ( ( F ` n ) O ( G ` n ) ) )
Assertion lmcn2 
|- ( ph -> H ( ~~>t ` N ) ( R O S ) )

Proof

Step Hyp Ref Expression
1 txlm.z 
 |-  Z = ( ZZ>= ` M )
2 txlm.m 
 |-  ( ph -> M e. ZZ )
3 txlm.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 txlm.k 
 |-  ( ph -> K e. ( TopOn ` Y ) )
5 txlm.f 
 |-  ( ph -> F : Z --> X )
6 txlm.g 
 |-  ( ph -> G : Z --> Y )
7 lmcn2.fl 
 |-  ( ph -> F ( ~~>t ` J ) R )
8 lmcn2.gl 
 |-  ( ph -> G ( ~~>t ` K ) S )
9 lmcn2.o 
 |-  ( ph -> O e. ( ( J tX K ) Cn N ) )
10 lmcn2.h 
 |-  H = ( n e. Z |-> ( ( F ` n ) O ( G ` n ) ) )
11 5 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. X )
12 6 ffvelcdmda 
 |-  ( ( ph /\ n e. Z ) -> ( G ` n ) e. Y )
13 11 12 opelxpd 
 |-  ( ( ph /\ n e. Z ) -> <. ( F ` n ) , ( G ` n ) >. e. ( X X. Y ) )
14 eqidd 
 |-  ( ph -> ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) )
15 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
16 3 4 15 syl2anc 
 |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
17 cntop2 
 |-  ( O e. ( ( J tX K ) Cn N ) -> N e. Top )
18 9 17 syl 
 |-  ( ph -> N e. Top )
19 toptopon2 
 |-  ( N e. Top <-> N e. ( TopOn ` U. N ) )
20 18 19 sylib 
 |-  ( ph -> N e. ( TopOn ` U. N ) )
21 cnf2 
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ N e. ( TopOn ` U. N ) /\ O e. ( ( J tX K ) Cn N ) ) -> O : ( X X. Y ) --> U. N )
22 16 20 9 21 syl3anc 
 |-  ( ph -> O : ( X X. Y ) --> U. N )
23 22 feqmptd 
 |-  ( ph -> O = ( x e. ( X X. Y ) |-> ( O ` x ) ) )
24 fveq2 
 |-  ( x = <. ( F ` n ) , ( G ` n ) >. -> ( O ` x ) = ( O ` <. ( F ` n ) , ( G ` n ) >. ) )
25 df-ov 
 |-  ( ( F ` n ) O ( G ` n ) ) = ( O ` <. ( F ` n ) , ( G ` n ) >. )
26 24 25 eqtr4di 
 |-  ( x = <. ( F ` n ) , ( G ` n ) >. -> ( O ` x ) = ( ( F ` n ) O ( G ` n ) ) )
27 13 14 23 26 fmptco 
 |-  ( ph -> ( O o. ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) ) = ( n e. Z |-> ( ( F ` n ) O ( G ` n ) ) ) )
28 27 10 eqtr4di 
 |-  ( ph -> ( O o. ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) ) = H )
29 eqid 
 |-  ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. )
30 1 2 3 4 5 6 29 txlm 
 |-  ( ph -> ( ( F ( ~~>t ` J ) R /\ G ( ~~>t ` K ) S ) <-> ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) ( ~~>t ` ( J tX K ) ) <. R , S >. ) )
31 7 8 30 mpbi2and 
 |-  ( ph -> ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) ( ~~>t ` ( J tX K ) ) <. R , S >. )
32 31 9 lmcn 
 |-  ( ph -> ( O o. ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. ) ) ( ~~>t ` N ) ( O ` <. R , S >. ) )
33 28 32 eqbrtrrd 
 |-  ( ph -> H ( ~~>t ` N ) ( O ` <. R , S >. ) )
34 df-ov 
 |-  ( R O S ) = ( O ` <. R , S >. )
35 33 34 breqtrrdi 
 |-  ( ph -> H ( ~~>t ` N ) ( R O S ) )