Theorem addccncf2

Description: Adding a constant is a continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypothesis	addccncf2.1	|- F = ( x e. A |-> ( B + x ) )
Assertion	addccncf2	|- ( ( A C_ CC /\ B e. CC ) -> F e. ( A -cn-> CC ) )

Proof

Step	Hyp	Ref	Expression
1		addccncf2.1	|- F = ( x e. A |-> ( B + x ) )
2		simpl	|- ( ( A C_ CC /\ B e. CC ) -> A C_ CC )
3		simpr	|- ( ( A C_ CC /\ B e. CC ) -> B e. CC )
4		ssidd	|- ( ( A C_ CC /\ B e. CC ) -> CC C_ CC )
5	2 3 4	constcncfg	|- ( ( A C_ CC /\ B e. CC ) -> ( x e. A |-> B ) e. ( A -cn-> CC ) )
6		ssid	|- CC C_ CC
7		cncfmptid	|- ( ( A C_ CC /\ CC C_ CC ) -> ( x e. A |-> x ) e. ( A -cn-> CC ) )
8	6 7	mpan2	|- ( A C_ CC -> ( x e. A |-> x ) e. ( A -cn-> CC ) )
9	8	adantr	|- ( ( A C_ CC /\ B e. CC ) -> ( x e. A |-> x ) e. ( A -cn-> CC ) )
10	5 9	addcncf	|- ( ( A C_ CC /\ B e. CC ) -> ( x e. A |-> ( B + x ) ) e. ( A -cn-> CC ) )
11	1 10	eqeltrid	|- ( ( A C_ CC /\ B e. CC ) -> F e. ( A -cn-> CC ) )