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

Metamath Proof Explorer

Theorem elcncf1di

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

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

Proof

Step	Hyp	Ref	Expression
1		elcncf1d.1	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		elcncf1d.2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺ ) → 𝑍 ∈ ℝ⁺ ) )
3		elcncf1d.3	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ⁺ ) → ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑍 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
4	2	imp	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺ ) ) → 𝑍 ∈ ℝ⁺ )
5		an32	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ⁺ ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺ ) ∧ 𝑤 ∈ 𝐴 ) )
6	5	bianass	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ⁺ ) ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺ ) ) ∧ 𝑤 ∈ 𝐴 ) )
7	3	imp	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ⁺ ) ) → ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑍 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
8	6 7	sylbir	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺ ) ) ∧ 𝑤 ∈ 𝐴 ) → ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑍 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
9	8	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺ ) ) → ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑍 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
10		breq2	⊢ ( 𝑧 = 𝑍 → ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 ↔ ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑍 ) )
11	10	rspceaimv	⊢ ( ( 𝑍 ∈ ℝ⁺ ∧ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑍 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
12	4 9 11	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ⁺ ) ) → ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
13	12	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
14	1 13	jca	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
15		elcncf	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ⁺ ∃ 𝑧 ∈ ℝ⁺ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )
16	14 15	syl5ibrcom	⊢ ( 𝜑 → ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ) )