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 φ J TopOn X
flfcnp2.k φ K TopOn Y
flfcnp2.l φ L Fil Z
flfcnp2.a φ x Z A X
flfcnp2.b φ x Z B Y
flfcnp2.r φ R J fLimf L x Z A
flfcnp2.s φ S K fLimf L x Z B
flfcnp2.o φ O J × t K CnP N R S
Assertion flfcnp2 φ R O S N fLimf L x Z A O B

Proof

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