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 φJTopOnX
flfcnp2.k φKTopOnY
flfcnp2.l φLFilZ
flfcnp2.a φxZAX
flfcnp2.b φxZBY
flfcnp2.r φRJfLimfLxZA
flfcnp2.s φSKfLimfLxZB
flfcnp2.o φOJ×tKCnPNRS
Assertion flfcnp2 φROSNfLimfLxZAOB

Proof

Step Hyp Ref Expression
1 flfcnp2.j φJTopOnX
2 flfcnp2.k φKTopOnY
3 flfcnp2.l φLFilZ
4 flfcnp2.a φxZAX
5 flfcnp2.b φxZBY
6 flfcnp2.r φRJfLimfLxZA
7 flfcnp2.s φSKfLimfLxZB
8 flfcnp2.o φOJ×tKCnPNRS
9 df-ov ROS=ORS
10 txtopon JTopOnXKTopOnYJ×tKTopOnX×Y
11 1 2 10 syl2anc φJ×tKTopOnX×Y
12 4 5 opelxpd φxZABX×Y
13 12 fmpttd φxZAB:ZX×Y
14 4 fmpttd φxZA:ZX
15 5 fmpttd φxZB:ZY
16 nfcv _yxZAxxZBx
17 nffvmpt1 _xxZAy
18 nffvmpt1 _xxZBy
19 17 18 nfop _xxZAyxZBy
20 fveq2 x=yxZAx=xZAy
21 fveq2 x=yxZBx=xZBy
22 20 21 opeq12d x=yxZAxxZBx=xZAyxZBy
23 16 19 22 cbvmpt xZxZAxxZBx=yZxZAyxZBy
24 1 2 3 14 15 23 txflf φRSJ×tKfLimfLxZxZAxxZBxRJfLimfLxZASKfLimfLxZB
25 6 7 24 mpbir2and φRSJ×tKfLimfLxZxZAxxZBx
26 simpr φxZxZ
27 eqid xZA=xZA
28 27 fvmpt2 xZAXxZAx=A
29 26 4 28 syl2anc φxZxZAx=A
30 eqid xZB=xZB
31 30 fvmpt2 xZBYxZBx=B
32 26 5 31 syl2anc φxZxZBx=B
33 29 32 opeq12d φxZxZAxxZBx=AB
34 33 mpteq2dva φxZxZAxxZBx=xZAB
35 34 fveq2d φJ×tKfLimfLxZxZAxxZBx=J×tKfLimfLxZAB
36 25 35 eleqtrd φRSJ×tKfLimfLxZAB
37 flfcnp J×tKTopOnX×YLFilZxZAB:ZX×YRSJ×tKfLimfLxZABOJ×tKCnPNRSORSNfLimfLOxZAB
38 11 3 13 36 8 37 syl32anc φORSNfLimfLOxZAB
39 eqidd φxZAB=xZAB
40 cnptop2 OJ×tKCnPNRSNTop
41 8 40 syl φNTop
42 toptopon2 NTopNTopOnN
43 41 42 sylib φNTopOnN
44 cnpf2 J×tKTopOnX×YNTopOnNOJ×tKCnPNRSO:X×YN
45 11 43 8 44 syl3anc φO:X×YN
46 45 feqmptd φO=yX×YOy
47 fveq2 y=ABOy=OAB
48 df-ov AOB=OAB
49 47 48 eqtr4di y=ABOy=AOB
50 12 39 46 49 fmptco φOxZAB=xZAOB
51 50 fveq2d φNfLimfLOxZAB=NfLimfLxZAOB
52 38 51 eleqtrd φORSNfLimfLxZAOB
53 9 52 eqeltrid φROSNfLimfLxZAOB