Theorem elcncf

Description: Membership in the set of continuous complex functions from A to B . (Contributed by Paul Chapman, 11-Oct-2007) (Revised by Mario Carneiro, 9-Nov-2013)

	Ref	Expression
Assertion	elcncf	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cncfval	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } )
2	1	eleq2d	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } ) )
3		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
4		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
5	3 4	oveq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) )
6	5	fveq2d	⊢ ( 𝑓 = 𝐹 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) )
7	6	breq1d	⊢ ( 𝑓 = 𝐹 → ( ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) )
8	7	imbi2d	⊢ ( 𝑓 = 𝐹 → ( ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
9	8	rexralbidv	⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
10	9	2ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
11	10	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } ↔ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
12	2 11	bitrdi	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )
13		cnex	⊢ ℂ ∈ V
14	13	ssex	⊢ ( 𝐵 ⊆ ℂ → 𝐵 ∈ V )
15	13	ssex	⊢ ( 𝐴 ⊆ ℂ → 𝐴 ∈ V )
16		elmapg	⊢ ( ( 𝐵 ∈ V ∧ 𝐴 ∈ V ) → ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )
17	14 15 16	syl2anr	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝐵 ) )
18	17	anbi1d	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( ( 𝐹 ∈ ( 𝐵 ↑m 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )
19	12 18	bitrd	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐹 ∈ ( 𝐴 –cn→ 𝐵 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑤 ) ) ) < 𝑦 ) ) ) )