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{\times }_{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 AFB\in S$$
Assertion	cncfmpt2ss	$$⊢\phi \to \left(x\in X⟼AFB\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{\times }_{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 AFB\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	fvmptelcdm	$$⊢\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	fvmptelcdm	$$⊢\left(\phi \wedge x\in X\right)\to B\in S$$
13	9 12 6	syl2anc	$$⊢\left(\phi \wedge x\in X\right)\to AFB\in S$$
14	13	fmpttd	$$⊢\phi \to \left(x\in X⟼AFB\right):X⟶S$$
15	2	a1i	$$⊢\phi \to F\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$
16		ssid	$$⊢ℂ\subseteq ℂ$$
17		cncfss	$$⊢\left(S\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to X\underset{cn}{⟶}S\subseteq X\underset{cn}{⟶}ℂ$$
18	5 16 17	mp2an	$$⊢X\underset{cn}{⟶}S\subseteq X\underset{cn}{⟶}ℂ$$
19	18 3	sselid	$$⊢\phi \to \left(x\in X⟼A\right):X\underset{cn}{⟶}ℂ$$
20	18 4	sselid	$$⊢\phi \to \left(x\in X⟼B\right):X\underset{cn}{⟶}ℂ$$
21	1 15 19 20	cncfmpt2f	$$⊢\phi \to \left(x\in X⟼AFB\right):X\underset{cn}{⟶}ℂ$$
22		cncfcdm	$$⊢\left(S\subseteq ℂ\wedge \left(x\in X⟼AFB\right):X\underset{cn}{⟶}ℂ\right)\to \left(\left(x\in X⟼AFB\right):X\underset{cn}{⟶}S\leftrightarrow \left(x\in X⟼AFB\right):X⟶S\right)$$
23	5 21 22	sylancr	$$⊢\phi \to \left(\left(x\in X⟼AFB\right):X\underset{cn}{⟶}S\leftrightarrow \left(x\in X⟼AFB\right):X⟶S\right)$$
24	14 23	mpbird	$$⊢\phi \to \left(x\in X⟼AFB\right):X\underset{cn}{⟶}S$$