Metamath Proof Explorer


Theorem cncfmpt2ss

Description: Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Hypotheses cncfmpt2ss.1
|- J = ( TopOpen ` CCfld )
cncfmpt2ss.2
|- F e. ( ( J tX J ) Cn J )
cncfmpt2ss.3
|- ( ph -> ( x e. X |-> A ) e. ( X -cn-> S ) )
cncfmpt2ss.4
|- ( ph -> ( x e. X |-> B ) e. ( X -cn-> S ) )
cncfmpt2ss.5
|- S C_ CC
cncfmpt2ss.6
|- ( ( A e. S /\ B e. S ) -> ( A F B ) e. S )
Assertion cncfmpt2ss
|- ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> S ) )

Proof

Step Hyp Ref Expression
1 cncfmpt2ss.1
 |-  J = ( TopOpen ` CCfld )
2 cncfmpt2ss.2
 |-  F e. ( ( J tX J ) Cn J )
3 cncfmpt2ss.3
 |-  ( ph -> ( x e. X |-> A ) e. ( X -cn-> S ) )
4 cncfmpt2ss.4
 |-  ( ph -> ( x e. X |-> B ) e. ( X -cn-> S ) )
5 cncfmpt2ss.5
 |-  S C_ CC
6 cncfmpt2ss.6
 |-  ( ( A e. S /\ B e. S ) -> ( A F B ) e. S )
7 cncff
 |-  ( ( x e. X |-> A ) e. ( X -cn-> S ) -> ( x e. X |-> A ) : X --> S )
8 3 7 syl
 |-  ( ph -> ( x e. X |-> A ) : X --> S )
9 8 fvmptelrn
 |-  ( ( ph /\ x e. X ) -> A e. S )
10 cncff
 |-  ( ( x e. X |-> B ) e. ( X -cn-> S ) -> ( x e. X |-> B ) : X --> S )
11 4 10 syl
 |-  ( ph -> ( x e. X |-> B ) : X --> S )
12 11 fvmptelrn
 |-  ( ( ph /\ x e. X ) -> B e. S )
13 9 12 6 syl2anc
 |-  ( ( ph /\ x e. X ) -> ( A F B ) e. S )
14 13 fmpttd
 |-  ( ph -> ( x e. X |-> ( A F B ) ) : X --> S )
15 2 a1i
 |-  ( ph -> F e. ( ( J tX J ) Cn J ) )
16 ssid
 |-  CC C_ CC
17 cncfss
 |-  ( ( S C_ CC /\ CC C_ CC ) -> ( X -cn-> S ) C_ ( X -cn-> CC ) )
18 5 16 17 mp2an
 |-  ( X -cn-> S ) C_ ( X -cn-> CC )
19 18 3 sselid
 |-  ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) )
20 18 4 sselid
 |-  ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) )
21 1 15 19 20 cncfmpt2f
 |-  ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) )
22 cncffvrn
 |-  ( ( S C_ CC /\ ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) ) -> ( ( x e. X |-> ( A F B ) ) e. ( X -cn-> S ) <-> ( x e. X |-> ( A F B ) ) : X --> S ) )
23 5 21 22 sylancr
 |-  ( ph -> ( ( x e. X |-> ( A F B ) ) e. ( X -cn-> S ) <-> ( x e. X |-> ( A F B ) ) : X --> S ) )
24 14 23 mpbird
 |-  ( ph -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> S ) )