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

Metamath Proof Explorer

Theorem cncfmpt2f

Description: Composition of continuous functions. -cn-> analogue of cnmpt12f . (Contributed by Mario Carneiro, 3-Sep-2014)

Ref Expression
Hypotheses cncfmpt2f.1 
|- J = ( TopOpen ` CCfld )
cncfmpt2f.2 
|- ( ph -> F e. ( ( J tX J ) Cn J ) )
cncfmpt2f.3 
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
cncfmpt2f.4 
|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )
Assertion cncfmpt2f 
|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 cncfmpt2f.1 
 |-  J = ( TopOpen ` CCfld )
2 cncfmpt2f.2 
 |-  ( ph -> F e. ( ( J tX J ) Cn J ) )
3 cncfmpt2f.3 
 |-  ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
4 cncfmpt2f.4 
 |-  ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )
5 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
6 cncfrss 
 |-  ( ( x e. X |-> A ) e. ( X -cn-> CC ) -> X C_ CC )
7 3 6 syl 
 |-  ( ph -> X C_ CC )
8 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ X C_ CC ) -> ( J |`t X ) e. ( TopOn ` X ) )
9 5 7 8 sylancr 
 |-  ( ph -> ( J |`t X ) e. ( TopOn ` X ) )
10 ssid 
 |-  CC C_ CC
11 eqid 
 |-  ( J |`t X ) = ( J |`t X )
12 5 toponrestid 
 |-  J = ( J |`t CC )
13 1 11 12 cncfcn 
 |-  ( ( X C_ CC /\ CC C_ CC ) -> ( X -cn-> CC ) = ( ( J |`t X ) Cn J ) )
14 7 10 13 sylancl 
 |-  ( ph -> ( X -cn-> CC ) = ( ( J |`t X ) Cn J ) )
15 3 14 eleqtrd 
 |-  ( ph -> ( x e. X |-> A ) e. ( ( J |`t X ) Cn J ) )
16 4 14 eleqtrd 
 |-  ( ph -> ( x e. X |-> B ) e. ( ( J |`t X ) Cn J ) )
17 9 15 16 2 cnmpt12f 
 |-  ( ph -> ( x e. X |-> ( A F B ) ) e. ( ( J |`t X ) Cn J ) )
18 17 14 eleqtrrd 
 |-  ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) )