Metamath Proof Explorer


Theorem cnextfun

Description: If the target space is Hausdorff, a continuous extension is a function. (Contributed by Thierry Arnoux, 20-Dec-2017)

Ref Expression
Hypotheses cnextfrel.1 C=J
cnextfrel.2 B=K
Assertion cnextfun JTopKHausF:ABACFunJCnExtKF

Proof

Step Hyp Ref Expression
1 cnextfrel.1 C=J
2 cnextfrel.2 B=K
3 haustop KHausKTop
4 1 2 cnextrel JTopKTopF:ABACRelJCnExtKF
5 3 4 sylanl2 JTopKHausF:ABACRelJCnExtKF
6 simpllr JTopKHausF:ABACxclsJAKHaus
7 1 toptopon JTopJTopOnC
8 7 biimpi JTopJTopOnC
9 8 ad3antrrr JTopKHausF:ABACxclsJAJTopOnC
10 simplrr JTopKHausF:ABACxclsJAAC
11 9 7 sylibr JTopKHausF:ABACxclsJAJTop
12 1 clsss3 JTopACclsJAC
13 11 10 12 syl2anc JTopKHausF:ABACxclsJAclsJAC
14 simpr JTopKHausF:ABACxclsJAxclsJA
15 13 14 sseldd JTopKHausF:ABACxclsJAxC
16 trnei JTopOnCACxCxclsJAneiJx𝑡AFilA
17 16 biimpa JTopOnCACxCxclsJAneiJx𝑡AFilA
18 9 10 15 14 17 syl31anc JTopKHausF:ABACxclsJAneiJx𝑡AFilA
19 simplrl JTopKHausF:ABACxclsJAF:AB
20 2 hausflf KHausneiJx𝑡AFilAF:AB*yyKfLimfneiJx𝑡AF
21 6 18 19 20 syl3anc JTopKHausF:ABACxclsJA*yyKfLimfneiJx𝑡AF
22 21 ex JTopKHausF:ABACxclsJA*yyKfLimfneiJx𝑡AF
23 22 alrimiv JTopKHausF:ABACxxclsJA*yyKfLimfneiJx𝑡AF
24 moanimv *yxclsJAyKfLimfneiJx𝑡AFxclsJA*yyKfLimfneiJx𝑡AF
25 24 albii x*yxclsJAyKfLimfneiJx𝑡AFxxclsJA*yyKfLimfneiJx𝑡AF
26 23 25 sylibr JTopKHausF:ABACx*yxclsJAyKfLimfneiJx𝑡AF
27 df-br xJCnExtKFyxyJCnExtKF
28 27 a1i JTopKHausF:ABACxJCnExtKFyxyJCnExtKF
29 1 2 cnextfval JTopKTopF:ABACJCnExtKF=xclsJAx×KfLimfneiJx𝑡AF
30 3 29 sylanl2 JTopKHausF:ABACJCnExtKF=xclsJAx×KfLimfneiJx𝑡AF
31 30 eleq2d JTopKHausF:ABACxyJCnExtKFxyxclsJAx×KfLimfneiJx𝑡AF
32 opeliunxp xyxclsJAx×KfLimfneiJx𝑡AFxclsJAyKfLimfneiJx𝑡AF
33 32 a1i JTopKHausF:ABACxyxclsJAx×KfLimfneiJx𝑡AFxclsJAyKfLimfneiJx𝑡AF
34 28 31 33 3bitrd JTopKHausF:ABACxJCnExtKFyxclsJAyKfLimfneiJx𝑡AF
35 34 mobidv JTopKHausF:ABAC*yxJCnExtKFy*yxclsJAyKfLimfneiJx𝑡AF
36 35 albidv JTopKHausF:ABACx*yxJCnExtKFyx*yxclsJAyKfLimfneiJx𝑡AF
37 26 36 mpbird JTopKHausF:ABACx*yxJCnExtKFy
38 dffun6 FunJCnExtKFRelJCnExtKFx*yxJCnExtKFy
39 5 37 38 sylanbrc JTopKHausF:ABACFunJCnExtKF