Description: A constant function is a continuous function on CC . (Contributed by Jeff Madsen, 2-Sep-2009) (Moved into main set.mm as cncfmptc and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | constcncf.1 | |- F = ( x e. CC |-> A ) |
|
| Assertion | constcncf | |- ( A e. CC -> F e. ( CC -cn-> CC ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | constcncf.1 | |- F = ( x e. CC |-> A ) |
|
| 2 | ssid | |- CC C_ CC |
|
| 3 | cncfmptc | |- ( ( A e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) ) |
|
| 4 | 2 2 3 | mp3an23 | |- ( A e. CC -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) ) |
| 5 | 1 4 | eqeltrid | |- ( A e. CC -> F e. ( CC -cn-> CC ) ) |