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

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 fvmptelcdm 
 |-  ( ( 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 fvmptelcdm 
 |-  ( ( 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 cncfcdm 
 |-  ( ( 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 ) )