Theorem add1cncf

Description: Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	add1cncf.a	|- ( ph -> A e. CC )
	add1cncf.f	|- F = ( x e. CC |-> ( x + A ) )
Assertion	add1cncf	|- ( ph -> F e. ( CC -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		add1cncf.a	|- ( ph -> A e. CC )
2		add1cncf.f	|- F = ( x e. CC |-> ( x + A ) )
3		ssid	|- CC C_ CC
4		cncfmptid	|- ( ( CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
5	3 3 4	mp2an	|- ( x e. CC |-> x ) e. ( CC -cn-> CC )
6	5	a1i	|- ( ph -> ( x e. CC |-> x ) e. ( CC -cn-> CC ) )
7		id	|- ( A e. CC -> A e. CC )
8	3	a1i	|- ( A e. CC -> CC C_ CC )
9		cncfmptc	|- ( ( A e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
10	7 8 8 9	syl3anc	|- ( A e. CC -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
11	1 10	syl	|- ( ph -> ( x e. CC |-> A ) e. ( CC -cn-> CC ) )
12	6 11	addcncf	|- ( ph -> ( x e. CC |-> ( x + A ) ) e. ( CC -cn-> CC ) )
13	2 12	eqeltrid	|- ( ph -> F e. ( CC -cn-> CC ) )