Metamath Proof Explorer


Theorem idcncfg

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 ) )

Proof

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 ) )