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

Metamath Proof Explorer

Theorem cncfmptss

Description: A continuous complex function restricted to a subset is continuous, using maps-to notation. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses cncfmptss.1 ⊢ Ⅎ 𝑥 𝐹
cncfmptss.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
cncfmptss.3 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
Assertion cncfmptss ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐶 –cn→ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cncfmptss.1 ⊢ Ⅎ 𝑥 𝐹
2 cncfmptss.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
3 cncfmptss.3 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4 3 resmptd ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ 𝐶 ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑦 ) ) )
5 cncff ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
6 2 5 syl ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 6 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) )
8 7 reseq1d ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) = ( ( 𝑦 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑦 ) ) ↾ 𝐶 ) )
9 nfcv ⊢ Ⅎ 𝑦 𝐹
10 nfcv ⊢ Ⅎ 𝑦 𝑥
11 9 10 nffv ⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 )
12 nfcv ⊢ Ⅎ 𝑥 𝑦
13 1 12 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
14 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
15 11 13 14 cbvmpt ⊢ ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑦 ) )
16 15 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑦 ) ) )
17 4 8 16 3eqtr4rd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ↾ 𝐶 ) )
18 rescncf ⊢ ( 𝐶 ⊆ 𝐴 → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → ( 𝐹 ↾ 𝐶 ) ∈ ( 𝐶 –cn→ 𝐵 ) ) )
19 3 2 18 sylc ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) ∈ ( 𝐶 –cn→ 𝐵 ) )
20 17 19 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐶 –cn→ 𝐵 ) )