Theorem cncfmpt2ss

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

	Ref	Expression
Hypotheses	cncfmpt2ss.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
	cncfmpt2ss.2	⊢ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
	cncfmpt2ss.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ 𝑆 ) )
	cncfmpt2ss.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ 𝑆 ) )
	cncfmpt2ss.5	⊢ 𝑆 ⊆ ℂ
	cncfmpt2ss.6	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )
Assertion	cncfmpt2ss	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		cncfmpt2ss.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		cncfmpt2ss.2	⊢ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
3		cncfmpt2ss.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ 𝑆 ) )
4		cncfmpt2ss.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ 𝑆 ) )
5		cncfmpt2ss.5	⊢ 𝑆 ⊆ ℂ
6		cncfmpt2ss.6	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )
7		cncff	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ 𝑆 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑆 )
8	3 7	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ 𝑆 )
9	8	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑆 )
10		cncff	⊢ ( ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ 𝑆 ) → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ 𝑆 )
11	4 10	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) : 𝑋 ⟶ 𝑆 )
12	11	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑆 )
13	9 12 6	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 𝐹 𝐵 ) ∈ 𝑆 )
14	13	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) : 𝑋 ⟶ 𝑆 )
15	2	a1i	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
16		ssid	⊢ ℂ ⊆ ℂ
17		cncfss	⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑋 –cn→ 𝑆 ) ⊆ ( 𝑋 –cn→ ℂ ) )
18	5 16 17	mp2an	⊢ ( 𝑋 –cn→ 𝑆 ) ⊆ ( 𝑋 –cn→ ℂ )
19	18 3	sselid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ∈ ( 𝑋 –cn→ ℂ ) )
20	18 4	sselid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) ∈ ( 𝑋 –cn→ ℂ ) )
21	1 15 19 20	cncfmpt2f	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) )
22		cncffvrn	⊢ ( ( 𝑆 ⊆ ℂ ∧ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ ℂ ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) : 𝑋 ⟶ 𝑆 ) )
23	5 21 22	sylancr	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ 𝑆 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) : 𝑋 ⟶ 𝑆 ) )
24	14 23	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 𝐹 𝐵 ) ) ∈ ( 𝑋 –cn→ 𝑆 ) )