Metamath Proof Explorer


Theorem cnprest

Description: Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014)

Ref Expression
Hypotheses cnprest.1 X=J
cnprest.2 Y=K
Assertion cnprest JTopAXPintJAF:XYFJCnPKPFAJ𝑡ACnPKP

Proof

Step Hyp Ref Expression
1 cnprest.1 X=J
2 cnprest.2 Y=K
3 cnptop2 FJCnPKPKTop
4 3 a1i JTopAXPintJAF:XYFJCnPKPKTop
5 cnptop2 FAJ𝑡ACnPKPKTop
6 5 a1i JTopAXPintJAF:XYFAJ𝑡ACnPKPKTop
7 1 ntrss2 JTopAXintJAA
8 7 3ad2ant1 JTopAXPintJAF:XYKTopintJAA
9 simp2l JTopAXPintJAF:XYKTopPintJA
10 8 9 sseldd JTopAXPintJAF:XYKTopPA
11 10 fvresd JTopAXPintJAF:XYKTopFAP=FP
12 11 eqcomd JTopAXPintJAF:XYKTopFP=FAP
13 12 eleq1d JTopAXPintJAF:XYKTopFPyFAPy
14 inss1 xAx
15 imass2 xAxFxAFx
16 sstr2 FxAFxFxyFxAy
17 14 15 16 mp2b FxyFxAy
18 17 anim2i PxFxyPxFxAy
19 18 reximi xJPxFxyxJPxFxAy
20 simp1l JTopAXPintJAF:XYKTopJTop
21 1 ntropn JTopAXintJAJ
22 21 3ad2ant1 JTopAXPintJAF:XYKTopintJAJ
23 inopn JTopxJintJAJxintJAJ
24 23 3com23 JTopintJAJxJxintJAJ
25 24 3expia JTopintJAJxJxintJAJ
26 20 22 25 syl2anc JTopAXPintJAF:XYKTopxJxintJAJ
27 elin PxintJAPxPintJA
28 27 simplbi2com PintJAPxPxintJA
29 9 28 syl JTopAXPintJAF:XYKTopPxPxintJA
30 sslin intJAAxintJAxA
31 8 30 syl JTopAXPintJAF:XYKTopxintJAxA
32 imass2 xintJAxAFxintJAFxA
33 31 32 syl JTopAXPintJAF:XYKTopFxintJAFxA
34 sstr2 FxintJAFxAFxAyFxintJAy
35 33 34 syl JTopAXPintJAF:XYKTopFxAyFxintJAy
36 29 35 anim12d JTopAXPintJAF:XYKTopPxFxAyPxintJAFxintJAy
37 26 36 anim12d JTopAXPintJAF:XYKTopxJPxFxAyxintJAJPxintJAFxintJAy
38 eleq2 z=xintJAPzPxintJA
39 imaeq2 z=xintJAFz=FxintJA
40 39 sseq1d z=xintJAFzyFxintJAy
41 38 40 anbi12d z=xintJAPzFzyPxintJAFxintJAy
42 41 rspcev xintJAJPxintJAFxintJAyzJPzFzy
43 37 42 syl6 JTopAXPintJAF:XYKTopxJPxFxAyzJPzFzy
44 43 expdimp JTopAXPintJAF:XYKTopxJPxFxAyzJPzFzy
45 44 rexlimdva JTopAXPintJAF:XYKTopxJPxFxAyzJPzFzy
46 eleq2 z=xPzPx
47 imaeq2 z=xFz=Fx
48 47 sseq1d z=xFzyFxy
49 46 48 anbi12d z=xPzFzyPxFxy
50 49 cbvrexvw zJPzFzyxJPxFxy
51 45 50 syl6ib JTopAXPintJAF:XYKTopxJPxFxAyxJPxFxy
52 19 51 impbid2 JTopAXPintJAF:XYKTopxJPxFxyxJPxFxAy
53 vex xV
54 53 inex1 xAV
55 54 a1i JTopAXPintJAF:XYKTopxJxAV
56 20 uniexd JTopAXPintJAF:XYKTopJV
57 simp1r JTopAXPintJAF:XYKTopAX
58 57 1 sseqtrdi JTopAXPintJAF:XYKTopAJ
59 56 58 ssexd JTopAXPintJAF:XYKTopAV
60 elrest JTopAVzJ𝑡AxJz=xA
61 20 59 60 syl2anc JTopAXPintJAF:XYKTopzJ𝑡AxJz=xA
62 eleq2 z=xAPzPxA
63 elin PxAPxPA
64 63 rbaib PAPxAPx
65 10 64 syl JTopAXPintJAF:XYKTopPxAPx
66 62 65 sylan9bbr JTopAXPintJAF:XYKTopz=xAPzPx
67 simpr JTopAXPintJAF:XYKTopz=xAz=xA
68 67 imaeq2d JTopAXPintJAF:XYKTopz=xAFAz=FAxA
69 inss2 xAA
70 resima2 xAAFAxA=FxA
71 69 70 ax-mp FAxA=FxA
72 68 71 eqtrdi JTopAXPintJAF:XYKTopz=xAFAz=FxA
73 72 sseq1d JTopAXPintJAF:XYKTopz=xAFAzyFxAy
74 66 73 anbi12d JTopAXPintJAF:XYKTopz=xAPzFAzyPxFxAy
75 55 61 74 rexxfr2d JTopAXPintJAF:XYKTopzJ𝑡APzFAzyxJPxFxAy
76 52 75 bitr4d JTopAXPintJAF:XYKTopxJPxFxyzJ𝑡APzFAzy
77 13 76 imbi12d JTopAXPintJAF:XYKTopFPyxJPxFxyFAPyzJ𝑡APzFAzy
78 77 ralbidv JTopAXPintJAF:XYKTopyKFPyxJPxFxyyKFAPyzJ𝑡APzFAzy
79 simp2r JTopAXPintJAF:XYKTopF:XY
80 simp3 JTopAXPintJAF:XYKTopKTop
81 57 10 sseldd JTopAXPintJAF:XYKTopPX
82 1 2 iscnp2 FJCnPKPJTopKTopPXF:XYyKFPyxJPxFxy
83 82 baib JTopKTopPXFJCnPKPF:XYyKFPyxJPxFxy
84 20 80 81 83 syl3anc JTopAXPintJAF:XYKTopFJCnPKPF:XYyKFPyxJPxFxy
85 79 84 mpbirand JTopAXPintJAF:XYKTopFJCnPKPyKFPyxJPxFxy
86 79 57 fssresd JTopAXPintJAF:XYKTopFA:AY
87 1 toptopon JTopJTopOnX
88 20 87 sylib JTopAXPintJAF:XYKTopJTopOnX
89 resttopon JTopOnXAXJ𝑡ATopOnA
90 88 57 89 syl2anc JTopAXPintJAF:XYKTopJ𝑡ATopOnA
91 2 toptopon KTopKTopOnY
92 80 91 sylib JTopAXPintJAF:XYKTopKTopOnY
93 iscnp J𝑡ATopOnAKTopOnYPAFAJ𝑡ACnPKPFA:AYyKFAPyzJ𝑡APzFAzy
94 90 92 10 93 syl3anc JTopAXPintJAF:XYKTopFAJ𝑡ACnPKPFA:AYyKFAPyzJ𝑡APzFAzy
95 86 94 mpbirand JTopAXPintJAF:XYKTopFAJ𝑡ACnPKPyKFAPyzJ𝑡APzFAzy
96 78 85 95 3bitr4d JTopAXPintJAF:XYKTopFJCnPKPFAJ𝑡ACnPKP
97 96 3expia JTopAXPintJAF:XYKTopFJCnPKPFAJ𝑡ACnPKP
98 4 6 97 pm5.21ndd JTopAXPintJAF:XYFJCnPKPFAJ𝑡ACnPKP