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 | |
|
cnextfrel.2 | |
||
Assertion | cnextfun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnextfrel.1 | |
|
2 | cnextfrel.2 | |
|
3 | haustop | |
|
4 | 1 2 | cnextrel | |
5 | 3 4 | sylanl2 | |
6 | simpllr | |
|
7 | 1 | toptopon | |
8 | 7 | biimpi | |
9 | 8 | ad3antrrr | |
10 | simplrr | |
|
11 | 9 7 | sylibr | |
12 | 1 | clsss3 | |
13 | 11 10 12 | syl2anc | |
14 | simpr | |
|
15 | 13 14 | sseldd | |
16 | trnei | |
|
17 | 16 | biimpa | |
18 | 9 10 15 14 17 | syl31anc | |
19 | simplrl | |
|
20 | 2 | hausflf | |
21 | 6 18 19 20 | syl3anc | |
22 | 21 | ex | |
23 | 22 | alrimiv | |
24 | moanimv | |
|
25 | 24 | albii | |
26 | 23 25 | sylibr | |
27 | df-br | |
|
28 | 27 | a1i | |
29 | 1 2 | cnextfval | |
30 | 3 29 | sylanl2 | |
31 | 30 | eleq2d | |
32 | opeliunxp | |
|
33 | 32 | a1i | |
34 | 28 31 33 | 3bitrd | |
35 | 34 | mobidv | |
36 | 35 | albidv | |
37 | 26 36 | mpbird | |
38 | dffun6 | |
|
39 | 5 37 38 | sylanbrc | |