Theorem elcncf1ii

Description: Membership in the set of continuous complex functions from A to B . (Contributed by Paul Chapman, 26-Nov-2007)

	Ref	Expression
Hypotheses	elcncf1i.1	⊢ 𝐹 : 𝐴 ⟶ 𝐵
	elcncf1i.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) → 𝑍 ∈ ℝ+ )
	elcncf1i.3	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑍 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
Assertion	elcncf1ii	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elcncf1i.1	⊢ 𝐹 : 𝐴 ⟶ 𝐵
2		elcncf1i.2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) → 𝑍 ∈ ℝ+ )
3		elcncf1i.3	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑍 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
4	1	a1i	⊢ ( ⊤ → 𝐹 : 𝐴 ⟶ 𝐵 )
5	2	a1i	⊢ ( ⊤ → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) → 𝑍 ∈ ℝ+ ) )
6	3	a1i	⊢ ( ⊤ → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑍 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
7	4 5 6	elcncf1di	⊢ ( ⊤ → ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) )
8	7	mptru	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) )