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 ) ) ) )