Description: The identity function is a continuous function on CC . (Contributed by Jeff Madsen, 11-Jun-2010) (Moved into main set.mm as cncfmptid and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | idcncf.1 | |- F = ( x e. CC |-> x ) |
|
| Assertion | idcncf | |- F e. ( CC -cn-> CC ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | idcncf.1 | |- F = ( x e. CC |-> x ) |
|
| 2 | ssid | |- CC C_ CC |
|
| 3 | cncfmptid | |- ( ( CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) ) |
|
| 4 | 2 2 3 | mp2an | |- ( x e. CC |-> x ) e. ( CC -cn-> CC ) |
| 5 | 1 4 | eqeltri | |- F e. ( CC -cn-> CC ) |