Theorem addccncf

Description: Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Hypothesis	addccncf.1	|- F = ( x e. CC |-> ( x + A ) )
Assertion	addccncf	|- ( A e. CC -> F e. ( CC -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		addccncf.1	|- F = ( x e. CC |-> ( x + A ) )
2		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3	2	addcn	|- + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
4	3	a1i	|- ( A e. CC -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
5		ssid	|- CC C_ CC
6		cncfmptid	|- ( ( CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
7	5 5 6	mp2an	|- ( x e. CC |-> x ) e. ( CC -cn-> CC )
8	7	a1i	|- ( A e. CC -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
9		cncfmptc	|- ( ( A e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
10	5 5 9	mp3an23	|- ( A e. CC -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
11	2 4 8 10	cncfmpt2f	|- ( A e. CC -> ( x e. CC |-> ( x + A ) ) e. ( CC -cn-> CC ) )
12	1 11	eqeltrid	|- ( A e. CC -> F e. ( CC -cn-> CC ) )