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

Metamath Proof Explorer

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→ 𝐵 ) )