Metamath Proof Explorer


Theorem flfcnp2

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, 19-Sep-2015)

Ref Expression
Hypotheses flfcnp2.j
|- ( ph -> J e. ( TopOn ` X ) )
flfcnp2.k
|- ( ph -> K e. ( TopOn ` Y ) )
flfcnp2.l
|- ( ph -> L e. ( Fil ` Z ) )
flfcnp2.a
|- ( ( ph /\ x e. Z ) -> A e. X )
flfcnp2.b
|- ( ( ph /\ x e. Z ) -> B e. Y )
flfcnp2.r
|- ( ph -> R e. ( ( J fLimf L ) ` ( x e. Z |-> A ) ) )
flfcnp2.s
|- ( ph -> S e. ( ( K fLimf L ) ` ( x e. Z |-> B ) ) )
flfcnp2.o
|- ( ph -> O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) )
Assertion flfcnp2
|- ( ph -> ( R O S ) e. ( ( N fLimf L ) ` ( x e. Z |-> ( A O B ) ) ) )

Proof

Step Hyp Ref Expression
1 flfcnp2.j
 |-  ( ph -> J e. ( TopOn ` X ) )
2 flfcnp2.k
 |-  ( ph -> K e. ( TopOn ` Y ) )
3 flfcnp2.l
 |-  ( ph -> L e. ( Fil ` Z ) )
4 flfcnp2.a
 |-  ( ( ph /\ x e. Z ) -> A e. X )
5 flfcnp2.b
 |-  ( ( ph /\ x e. Z ) -> B e. Y )
6 flfcnp2.r
 |-  ( ph -> R e. ( ( J fLimf L ) ` ( x e. Z |-> A ) ) )
7 flfcnp2.s
 |-  ( ph -> S e. ( ( K fLimf L ) ` ( x e. Z |-> B ) ) )
8 flfcnp2.o
 |-  ( ph -> O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) )
9 df-ov
 |-  ( R O S ) = ( O ` <. R , S >. )
10 txtopon
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
11 1 2 10 syl2anc
 |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
12 4 5 opelxpd
 |-  ( ( ph /\ x e. Z ) -> <. A , B >. e. ( X X. Y ) )
13 12 fmpttd
 |-  ( ph -> ( x e. Z |-> <. A , B >. ) : Z --> ( X X. Y ) )
14 4 fmpttd
 |-  ( ph -> ( x e. Z |-> A ) : Z --> X )
15 5 fmpttd
 |-  ( ph -> ( x e. Z |-> B ) : Z --> Y )
16 nfcv
 |-  F/_ y <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >.
17 nffvmpt1
 |-  F/_ x ( ( x e. Z |-> A ) ` y )
18 nffvmpt1
 |-  F/_ x ( ( x e. Z |-> B ) ` y )
19 17 18 nfop
 |-  F/_ x <. ( ( x e. Z |-> A ) ` y ) , ( ( x e. Z |-> B ) ` y ) >.
20 fveq2
 |-  ( x = y -> ( ( x e. Z |-> A ) ` x ) = ( ( x e. Z |-> A ) ` y ) )
21 fveq2
 |-  ( x = y -> ( ( x e. Z |-> B ) ` x ) = ( ( x e. Z |-> B ) ` y ) )
22 20 21 opeq12d
 |-  ( x = y -> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. = <. ( ( x e. Z |-> A ) ` y ) , ( ( x e. Z |-> B ) ` y ) >. )
23 16 19 22 cbvmpt
 |-  ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) = ( y e. Z |-> <. ( ( x e. Z |-> A ) ` y ) , ( ( x e. Z |-> B ) ` y ) >. )
24 1 2 3 14 15 23 txflf
 |-  ( ph -> ( <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) ) <-> ( R e. ( ( J fLimf L ) ` ( x e. Z |-> A ) ) /\ S e. ( ( K fLimf L ) ` ( x e. Z |-> B ) ) ) ) )
25 6 7 24 mpbir2and
 |-  ( ph -> <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) ) )
26 simpr
 |-  ( ( ph /\ x e. Z ) -> x e. Z )
27 eqid
 |-  ( x e. Z |-> A ) = ( x e. Z |-> A )
28 27 fvmpt2
 |-  ( ( x e. Z /\ A e. X ) -> ( ( x e. Z |-> A ) ` x ) = A )
29 26 4 28 syl2anc
 |-  ( ( ph /\ x e. Z ) -> ( ( x e. Z |-> A ) ` x ) = A )
30 eqid
 |-  ( x e. Z |-> B ) = ( x e. Z |-> B )
31 30 fvmpt2
 |-  ( ( x e. Z /\ B e. Y ) -> ( ( x e. Z |-> B ) ` x ) = B )
32 26 5 31 syl2anc
 |-  ( ( ph /\ x e. Z ) -> ( ( x e. Z |-> B ) ` x ) = B )
33 29 32 opeq12d
 |-  ( ( ph /\ x e. Z ) -> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. = <. A , B >. )
34 33 mpteq2dva
 |-  ( ph -> ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) = ( x e. Z |-> <. A , B >. ) )
35 34 fveq2d
 |-  ( ph -> ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. ( ( x e. Z |-> A ) ` x ) , ( ( x e. Z |-> B ) ` x ) >. ) ) = ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. A , B >. ) ) )
36 25 35 eleqtrd
 |-  ( ph -> <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. A , B >. ) ) )
37 flfcnp
 |-  ( ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ L e. ( Fil ` Z ) /\ ( x e. Z |-> <. A , B >. ) : Z --> ( X X. Y ) ) /\ ( <. R , S >. e. ( ( ( J tX K ) fLimf L ) ` ( x e. Z |-> <. A , B >. ) ) /\ O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) ) ) -> ( O ` <. R , S >. ) e. ( ( N fLimf L ) ` ( O o. ( x e. Z |-> <. A , B >. ) ) ) )
38 11 3 13 36 8 37 syl32anc
 |-  ( ph -> ( O ` <. R , S >. ) e. ( ( N fLimf L ) ` ( O o. ( x e. Z |-> <. A , B >. ) ) ) )
39 eqidd
 |-  ( ph -> ( x e. Z |-> <. A , B >. ) = ( x e. Z |-> <. A , B >. ) )
40 cnptop2
 |-  ( O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) -> N e. Top )
41 8 40 syl
 |-  ( ph -> N e. Top )
42 toptopon2
 |-  ( N e. Top <-> N e. ( TopOn ` U. N ) )
43 41 42 sylib
 |-  ( ph -> N e. ( TopOn ` U. N ) )
44 cnpf2
 |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ N e. ( TopOn ` U. N ) /\ O e. ( ( ( J tX K ) CnP N ) ` <. R , S >. ) ) -> O : ( X X. Y ) --> U. N )
45 11 43 8 44 syl3anc
 |-  ( ph -> O : ( X X. Y ) --> U. N )
46 45 feqmptd
 |-  ( ph -> O = ( y e. ( X X. Y ) |-> ( O ` y ) ) )
47 fveq2
 |-  ( y = <. A , B >. -> ( O ` y ) = ( O ` <. A , B >. ) )
48 df-ov
 |-  ( A O B ) = ( O ` <. A , B >. )
49 47 48 eqtr4di
 |-  ( y = <. A , B >. -> ( O ` y ) = ( A O B ) )
50 12 39 46 49 fmptco
 |-  ( ph -> ( O o. ( x e. Z |-> <. A , B >. ) ) = ( x e. Z |-> ( A O B ) ) )
51 50 fveq2d
 |-  ( ph -> ( ( N fLimf L ) ` ( O o. ( x e. Z |-> <. A , B >. ) ) ) = ( ( N fLimf L ) ` ( x e. Z |-> ( A O B ) ) ) )
52 38 51 eleqtrd
 |-  ( ph -> ( O ` <. R , S >. ) e. ( ( N fLimf L ) ` ( x e. Z |-> ( A O B ) ) ) )
53 9 52 eqeltrid
 |-  ( ph -> ( R O S ) e. ( ( N fLimf L ) ` ( x e. Z |-> ( A O B ) ) ) )