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 | |
|
flfcnp2.k | |
||
flfcnp2.l | |
||
flfcnp2.a | |
||
flfcnp2.b | |
||
flfcnp2.r | |
||
flfcnp2.s | |
||
flfcnp2.o | |
||
Assertion | flfcnp2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | flfcnp2.j | |
|
2 | flfcnp2.k | |
|
3 | flfcnp2.l | |
|
4 | flfcnp2.a | |
|
5 | flfcnp2.b | |
|
6 | flfcnp2.r | |
|
7 | flfcnp2.s | |
|
8 | flfcnp2.o | |
|
9 | df-ov | |
|
10 | txtopon | |
|
11 | 1 2 10 | syl2anc | |
12 | 4 5 | opelxpd | |
13 | 12 | fmpttd | |
14 | 4 | fmpttd | |
15 | 5 | fmpttd | |
16 | nfcv | |
|
17 | nffvmpt1 | |
|
18 | nffvmpt1 | |
|
19 | 17 18 | nfop | |
20 | fveq2 | |
|
21 | fveq2 | |
|
22 | 20 21 | opeq12d | |
23 | 16 19 22 | cbvmpt | |
24 | 1 2 3 14 15 23 | txflf | |
25 | 6 7 24 | mpbir2and | |
26 | simpr | |
|
27 | eqid | |
|
28 | 27 | fvmpt2 | |
29 | 26 4 28 | syl2anc | |
30 | eqid | |
|
31 | 30 | fvmpt2 | |
32 | 26 5 31 | syl2anc | |
33 | 29 32 | opeq12d | |
34 | 33 | mpteq2dva | |
35 | 34 | fveq2d | |
36 | 25 35 | eleqtrd | |
37 | flfcnp | |
|
38 | 11 3 13 36 8 37 | syl32anc | |
39 | eqidd | |
|
40 | cnptop2 | |
|
41 | 8 40 | syl | |
42 | toptopon2 | |
|
43 | 41 42 | sylib | |
44 | cnpf2 | |
|
45 | 11 43 8 44 | syl3anc | |
46 | 45 | feqmptd | |
47 | fveq2 | |
|
48 | df-ov | |
|
49 | 47 48 | eqtr4di | |
50 | 12 39 46 49 | fmptco | |
51 | 50 | fveq2d | |
52 | 38 51 | eleqtrd | |
53 | 9 52 | eqeltrid | |