Description: A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | cnconst2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconst6g | |
|
2 | 1 | 3ad2ant3 | |
3 | 2 | adantr | |
4 | simpll3 | |
|
5 | simplr | |
|
6 | fvconst2g | |
|
7 | 4 5 6 | syl2anc | |
8 | 7 | eleq1d | |
9 | simpll1 | |
|
10 | toponmax | |
|
11 | 9 10 | syl | |
12 | simplr | |
|
13 | df-ima | |
|
14 | ssid | |
|
15 | xpssres | |
|
16 | 14 15 | ax-mp | |
17 | 16 | rneqi | |
18 | rnxpss | |
|
19 | 17 18 | eqsstri | |
20 | simprr | |
|
21 | 20 | snssd | |
22 | 19 21 | sstrid | |
23 | 13 22 | eqsstrid | |
24 | eleq2 | |
|
25 | imaeq2 | |
|
26 | 25 | sseq1d | |
27 | 24 26 | anbi12d | |
28 | 27 | rspcev | |
29 | 11 12 23 28 | syl12anc | |
30 | 29 | expr | |
31 | 8 30 | sylbid | |
32 | 31 | ralrimiva | |
33 | simpl1 | |
|
34 | simpl2 | |
|
35 | simpr | |
|
36 | iscnp | |
|
37 | 33 34 35 36 | syl3anc | |
38 | 3 32 37 | mpbir2and | |
39 | 38 | ralrimiva | |
40 | cncnp | |
|
41 | 40 | 3adant3 | |
42 | 2 39 41 | mpbir2and | |