Metamath Proof Explorer


Theorem limccnp2

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, 28-Dec-2016)

Ref Expression
Hypotheses limccnp2.r φxARX
limccnp2.s φxASY
limccnp2.x φX
limccnp2.y φY
limccnp2.k K=TopOpenfld
limccnp2.j J=K×tK𝑡X×Y
limccnp2.c φCxARlimB
limccnp2.d φDxASlimB
limccnp2.h φHJCnPKCD
Assertion limccnp2 φCHDxARHSlimB

Proof

Step Hyp Ref Expression
1 limccnp2.r φxARX
2 limccnp2.s φxASY
3 limccnp2.x φX
4 limccnp2.y φY
5 limccnp2.k K=TopOpenfld
6 limccnp2.j J=K×tK𝑡X×Y
7 limccnp2.c φCxARlimB
8 limccnp2.d φDxASlimB
9 limccnp2.h φHJCnPKCD
10 eqid J=J
11 10 cnprcl HJCnPKCDCDJ
12 9 11 syl φCDJ
13 5 cnfldtopon KTopOn
14 txtopon KTopOnKTopOnK×tKTopOn×
15 13 13 14 mp2an K×tKTopOn×
16 xpss12 XYX×Y×
17 3 4 16 syl2anc φX×Y×
18 resttopon K×tKTopOn×X×Y×K×tK𝑡X×YTopOnX×Y
19 15 17 18 sylancr φK×tK𝑡X×YTopOnX×Y
20 6 19 eqeltrid φJTopOnX×Y
21 toponuni JTopOnX×YX×Y=J
22 20 21 syl φX×Y=J
23 12 22 eleqtrrd φCDX×Y
24 opelxp CDX×YCXDY
25 23 24 sylib φCXDY
26 25 simpld φCX
27 26 ad2antrr φxABx=BCX
28 simpll φxAB¬x=Bφ
29 simpr φxABxAB
30 elun xABxAxB
31 29 30 sylib φxABxAxB
32 31 ord φxAB¬xAxB
33 elsni xBx=B
34 32 33 syl6 φxAB¬xAx=B
35 34 con1d φxAB¬x=BxA
36 35 imp φxAB¬x=BxA
37 28 36 1 syl2anc φxAB¬x=BRX
38 27 37 ifclda φxABifx=BCRX
39 25 simprd φDY
40 39 ad2antrr φxABx=BDY
41 28 36 2 syl2anc φxAB¬x=BSY
42 40 41 ifclda φxABifx=BDSY
43 38 42 opelxpd φxABifx=BCRifx=BDSX×Y
44 eqidd φxABifx=BCRifx=BDS=xABifx=BCRifx=BDS
45 13 a1i φKTopOn
46 cnpf2 JTopOnX×YKTopOnHJCnPKCDH:X×Y
47 20 45 9 46 syl3anc φH:X×Y
48 47 feqmptd φH=yX×YHy
49 fveq2 y=ifx=BCRifx=BDSHy=Hifx=BCRifx=BDS
50 df-ov ifx=BCRHifx=BDS=Hifx=BCRifx=BDS
51 ovif12 ifx=BCRHifx=BDS=ifx=BCHDRHS
52 50 51 eqtr3i Hifx=BCRifx=BDS=ifx=BCHDRHS
53 49 52 eqtrdi y=ifx=BCRifx=BDSHy=ifx=BCHDRHS
54 43 44 48 53 fmptco φHxABifx=BCRifx=BDS=xABifx=BCHDRHS
55 eqid xAR=xAR
56 55 1 dmmptd φdomxAR=A
57 limcrcl CxARlimBxAR:domxARdomxARB
58 7 57 syl φxAR:domxARdomxARB
59 58 simp2d φdomxAR
60 56 59 eqsstrrd φA
61 58 simp3d φB
62 61 snssd φB
63 60 62 unssd φAB
64 resttopon KTopOnABK𝑡ABTopOnAB
65 13 63 64 sylancr φK𝑡ABTopOnAB
66 ssun2 BAB
67 snssg BBABBAB
68 61 67 syl φBABBAB
69 66 68 mpbiri φBAB
70 3 adantr φxAX
71 70 1 sseldd φxAR
72 eqid K𝑡AB=K𝑡AB
73 60 61 71 72 5 limcmpt φCxARlimBxABifx=BCRK𝑡ABCnPKB
74 7 73 mpbid φxABifx=BCRK𝑡ABCnPKB
75 4 adantr φxAY
76 75 2 sseldd φxAS
77 60 61 76 72 5 limcmpt φDxASlimBxABifx=BDSK𝑡ABCnPKB
78 8 77 mpbid φxABifx=BDSK𝑡ABCnPKB
79 65 45 45 69 74 78 txcnp φxABifx=BCRifx=BDSK𝑡ABCnPK×tKB
80 15 topontopi K×tKTop
81 80 a1i φK×tKTop
82 43 fmpttd φxABifx=BCRifx=BDS:ABX×Y
83 toponuni K𝑡ABTopOnABAB=K𝑡AB
84 65 83 syl φAB=K𝑡AB
85 84 feq2d φxABifx=BCRifx=BDS:ABX×YxABifx=BCRifx=BDS:K𝑡ABX×Y
86 82 85 mpbid φxABifx=BCRifx=BDS:K𝑡ABX×Y
87 eqid K𝑡AB=K𝑡AB
88 15 toponunii ×=K×tK
89 87 88 cnprest2 K×tKTopxABifx=BCRifx=BDS:K𝑡ABX×YX×Y×xABifx=BCRifx=BDSK𝑡ABCnPK×tKBxABifx=BCRifx=BDSK𝑡ABCnPK×tK𝑡X×YB
90 81 86 17 89 syl3anc φxABifx=BCRifx=BDSK𝑡ABCnPK×tKBxABifx=BCRifx=BDSK𝑡ABCnPK×tK𝑡X×YB
91 79 90 mpbid φxABifx=BCRifx=BDSK𝑡ABCnPK×tK𝑡X×YB
92 6 oveq2i K𝑡ABCnPJ=K𝑡ABCnPK×tK𝑡X×Y
93 92 fveq1i K𝑡ABCnPJB=K𝑡ABCnPK×tK𝑡X×YB
94 91 93 eleqtrrdi φxABifx=BCRifx=BDSK𝑡ABCnPJB
95 iftrue x=Bifx=BCR=C
96 iftrue x=Bifx=BDS=D
97 95 96 opeq12d x=Bifx=BCRifx=BDS=CD
98 eqid xABifx=BCRifx=BDS=xABifx=BCRifx=BDS
99 opex CDV
100 97 98 99 fvmpt BABxABifx=BCRifx=BDSB=CD
101 69 100 syl φxABifx=BCRifx=BDSB=CD
102 101 fveq2d φJCnPKxABifx=BCRifx=BDSB=JCnPKCD
103 9 102 eleqtrrd φHJCnPKxABifx=BCRifx=BDSB
104 cnpco xABifx=BCRifx=BDSK𝑡ABCnPJBHJCnPKxABifx=BCRifx=BDSBHxABifx=BCRifx=BDSK𝑡ABCnPKB
105 94 103 104 syl2anc φHxABifx=BCRifx=BDSK𝑡ABCnPKB
106 54 105 eqeltrrd φxABifx=BCHDRHSK𝑡ABCnPKB
107 47 adantr φxAH:X×Y
108 107 1 2 fovrnd φxARHS
109 60 61 108 72 5 limcmpt φCHDxARHSlimBxABifx=BCHDRHSK𝑡ABCnPKB
110 106 109 mpbird φCHDxARHSlimB