This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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