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

Metamath Proof Explorer

Theorem cncfmptssg

Description: A continuous complex function restricted to a subset is continuous, using maps-to notation. This theorem generalizes cncfmptss because it allows to establish a subset for the codomain also. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfmptssg.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐸 )
cncfmptssg.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
cncfmptssg.4 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
cncfmptssg.5 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐵 )
cncfmptssg.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐸 ∈ 𝐷 )
Assertion cncfmptssg ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 cncfmptssg.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐸 )
2 cncfmptssg.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )
3 cncfmptssg.4 ⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
4 cncfmptssg.5 ⊢ ( 𝜑 → 𝐷 ⊆ 𝐵 )
5 cncfmptssg.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝐸 ∈ 𝐷 )
6 5 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) : 𝐶 ⟶ 𝐷 )
7 cncfrss2 ⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐵 ⊆ ℂ )
8 2 7 syl ⊢ ( 𝜑 → 𝐵 ⊆ ℂ )
9 4 8 sstrd ⊢ ( 𝜑 → 𝐷 ⊆ ℂ )
10 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ 𝐴 )
11 1 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐸 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑥 ) = 𝐸 )
12 10 5 11 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑥 ) = 𝐸 )
13 12 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) )
14 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐸 )
15 1 14 nfcxfr ⊢ Ⅎ 𝑥 𝐹
16 15 2 3 cncfmptss ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ ( 𝐶 –cn→ 𝐵 ) )
17 13 16 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐵 ) )
18 cncfcdm ⊢ ( ( 𝐷 ⊆ ℂ ∧ ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐵 ) ) → ( ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) : 𝐶 ⟶ 𝐷 ) )
19 9 17 18 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) : 𝐶 ⟶ 𝐷 ) )
20 6 19 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐶 ↦ 𝐸 ) ∈ ( 𝐶 –cn→ 𝐷 ) )