Theorem cncfcdm

Description: Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 1-May-2015)

	Ref	Expression
Assertion	cncfcdm	⊢ ( ( 𝐶 ⊆ ℂ ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐶 ) ↔ 𝐹 : 𝐴 ⟶ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		cncfi	⊢ ( ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) )
2	1	3expb	⊢ ( ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) )
3	2	ralrimivva	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) )
4	3	adantl	⊢ ( ( 𝐶 ⊆ ℂ ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) )
5		cncfrss	⊢ ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) → 𝐴 ⊆ ℂ )
6		simpl	⊢ ( ( 𝐶 ⊆ ℂ ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → 𝐶 ⊆ ℂ )
7		elcncf2	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐶 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐶 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
8	5 6 7	syl2an2	⊢ ( ( 𝐶 ⊆ ℂ ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐶 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑤 ) − ( 𝐹 ‘ 𝑥 ) ) ) < 𝑦 ) ) ) )
9	4 8	mpbiran2d	⊢ ( ( 𝐶 ⊆ ℂ ∧ 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐶 ) ↔ 𝐹 : 𝐴 ⟶ 𝐶 ) )