# 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}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
cncfmpt2ss.2 ${⊢}{F}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
cncfmpt2ss.3 ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right):{X}\underset{cn}{⟶}{S}$
cncfmpt2ss.4 ${⊢}{\phi }\to \left({x}\in {X}⟼{B}\right):{X}\underset{cn}{⟶}{S}$
cncfmpt2ss.5 ${⊢}{S}\subseteq ℂ$
cncfmpt2ss.6 ${⊢}\left({A}\in {S}\wedge {B}\in {S}\right)\to {A}{F}{B}\in {S}$
Assertion cncfmpt2ss ${⊢}{\phi }\to \left({x}\in {X}⟼{A}{F}{B}\right):{X}\underset{cn}{⟶}{S}$

### Proof

Step Hyp Ref Expression
1 cncfmpt2ss.1 ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 cncfmpt2ss.2 ${⊢}{F}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
3 cncfmpt2ss.3 ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right):{X}\underset{cn}{⟶}{S}$
4 cncfmpt2ss.4 ${⊢}{\phi }\to \left({x}\in {X}⟼{B}\right):{X}\underset{cn}{⟶}{S}$
5 cncfmpt2ss.5 ${⊢}{S}\subseteq ℂ$
6 cncfmpt2ss.6 ${⊢}\left({A}\in {S}\wedge {B}\in {S}\right)\to {A}{F}{B}\in {S}$
7 cncff ${⊢}\left({x}\in {X}⟼{A}\right):{X}\underset{cn}{⟶}{S}\to \left({x}\in {X}⟼{A}\right):{X}⟶{S}$
8 3 7 syl ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right):{X}⟶{S}$
9 8 fvmptelrn ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}\in {S}$
10 cncff ${⊢}\left({x}\in {X}⟼{B}\right):{X}\underset{cn}{⟶}{S}\to \left({x}\in {X}⟼{B}\right):{X}⟶{S}$
11 4 10 syl ${⊢}{\phi }\to \left({x}\in {X}⟼{B}\right):{X}⟶{S}$
12 11 fvmptelrn ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {B}\in {S}$
13 9 12 6 syl2anc ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}{F}{B}\in {S}$
14 13 fmpttd ${⊢}{\phi }\to \left({x}\in {X}⟼{A}{F}{B}\right):{X}⟶{S}$
15 2 a1i ${⊢}{\phi }\to {F}\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
16 ssid ${⊢}ℂ\subseteq ℂ$
17 cncfss
18 5 16 17 mp2an
19 18 3 sseldi ${⊢}{\phi }\to \left({x}\in {X}⟼{A}\right):{X}\underset{cn}{⟶}ℂ$
20 18 4 sseldi ${⊢}{\phi }\to \left({x}\in {X}⟼{B}\right):{X}\underset{cn}{⟶}ℂ$
21 1 15 19 20 cncfmpt2f ${⊢}{\phi }\to \left({x}\in {X}⟼{A}{F}{B}\right):{X}\underset{cn}{⟶}ℂ$
22 cncffvrn ${⊢}\left({S}\subseteq ℂ\wedge \left({x}\in {X}⟼{A}{F}{B}\right):{X}\underset{cn}{⟶}ℂ\right)\to \left(\left({x}\in {X}⟼{A}{F}{B}\right):{X}\underset{cn}{⟶}{S}↔\left({x}\in {X}⟼{A}{F}{B}\right):{X}⟶{S}\right)$
23 5 21 22 sylancr ${⊢}{\phi }\to \left(\left({x}\in {X}⟼{A}{F}{B}\right):{X}\underset{cn}{⟶}{S}↔\left({x}\in {X}⟼{A}{F}{B}\right):{X}⟶{S}\right)$
24 14 23 mpbird ${⊢}{\phi }\to \left({x}\in {X}⟼{A}{F}{B}\right):{X}\underset{cn}{⟶}{S}$