Description: The identity function is a continuous function on CC . (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | idcncfg.a | |- ( ph -> A C_ B ) |
|
idcncfg.b | |- ( ph -> B C_ CC ) |
||
Assertion | idcncfg | |- ( ph -> ( x e. A |-> x ) e. ( A -cn-> B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idcncfg.a | |- ( ph -> A C_ B ) |
|
2 | idcncfg.b | |- ( ph -> B C_ CC ) |
|
3 | cncfmptid | |- ( ( A C_ B /\ B C_ CC ) -> ( x e. A |-> x ) e. ( A -cn-> B ) ) |
|
4 | 1 2 3 | syl2anc | |- ( ph -> ( x e. A |-> x ) e. ( A -cn-> B ) ) |