Theorem cncfval

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

	Ref	Expression
Assertion	cncfval	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } )

Proof

Step	Hyp	Ref	Expression
1		cnex	⊢ ℂ ∈ V
2	1	elpw2	⊢ ( 𝐴 ∈ 𝒫 ℂ ↔ 𝐴 ⊆ ℂ )
3	1	elpw2	⊢ ( 𝐵 ∈ 𝒫 ℂ ↔ 𝐵 ⊆ ℂ )
4		oveq2	⊢ ( 𝑎 = 𝐴 → ( 𝑏 ↑m 𝑎 ) = ( 𝑏 ↑m 𝐴 ) )
5		raleq	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑤 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
6	5	rexbidv	⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
7	6	ralbidv	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
8	7	raleqbi1dv	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) ) )
9	4 8	rabeqbidv	⊢ ( 𝑎 = 𝐴 → { 𝑓 ∈ ( 𝑏 ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } = { 𝑓 ∈ ( 𝑏 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } )
10		oveq1	⊢ ( 𝑏 = 𝐵 → ( 𝑏 ↑m 𝐴 ) = ( 𝐵 ↑m 𝐴 ) )
11	10	rabeqdv	⊢ ( 𝑏 = 𝐵 → { 𝑓 ∈ ( 𝑏 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } )
12		df-cncf	⊢ –cn→ = ( 𝑎 ∈ 𝒫 ℂ , 𝑏 ∈ 𝒫 ℂ ↦ { 𝑓 ∈ ( 𝑏 ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } )
13		ovex	⊢ ( 𝐵 ↑m 𝐴 ) ∈ V
14	13	rabex	⊢ { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } ∈ V
15	9 11 12 14	ovmpo	⊢ ( ( 𝐴 ∈ 𝒫 ℂ ∧ 𝐵 ∈ 𝒫 ℂ ) → ( 𝐴 –cn→ 𝐵 ) = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } )
16	2 3 15	syl2anbr	⊢ ( ( 𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ ) → ( 𝐴 –cn→ 𝐵 ) = { 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ∣ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ 𝐴 ( ( abs ‘ ( 𝑥 − 𝑤 ) ) < 𝑧 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑤 ) ) ) < 𝑦 ) } )