Definition df-cncf

Description: Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007)

	Ref	Expression
Assertion	df-cncf	⊢ –cn→ = ( 𝑎 ∈ 𝒫 ℂ , 𝑏 ∈ 𝒫 ℂ ↦ { 𝑓 ∈ ( 𝑏 ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccncf	⊢ –cn→
1		va	⊢ 𝑎
2		cc	⊢ ℂ
3	2	cpw	⊢ 𝒫 ℂ
4		vb	⊢ 𝑏
5		vf	⊢ 𝑓
6	4	cv	⊢ 𝑏
7		cmap	⊢ ↑m
8	1	cv	⊢ 𝑎
9	6 8 7	co	⊢ ( 𝑏 ↑m 𝑎 )
10		vx	⊢ 𝑥
11		ve	⊢ 𝑒
12		crp	⊢ ℝ+
13		vd	⊢ 𝑑
14		vy	⊢ 𝑦
15		cabs	⊢ abs
16	10	cv	⊢ 𝑥
17		cmin	⊢ −
18	14	cv	⊢ 𝑦
19	16 18 17	co	⊢ ( 𝑥 − 𝑦 )
20	19 15	cfv	⊢ ( abs ‘ ( 𝑥 − 𝑦 ) )
21		clt	⊢ <
22	13	cv	⊢ 𝑑
23	20 22 21	wbr	⊢ ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑
24	5	cv	⊢ 𝑓
25	16 24	cfv	⊢ ( 𝑓 ‘ 𝑥 )
26	18 24	cfv	⊢ ( 𝑓 ‘ 𝑦 )
27	25 26 17	co	⊢ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) )
28	27 15	cfv	⊢ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) )
29	11	cv	⊢ 𝑒
30	28 29 21	wbr	⊢ ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒
31	23 30	wi	⊢ ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒 )
32	31 14 8	wral	⊢ ∀ 𝑦 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒 )
33	32 13 12	wrex	⊢ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒 )
34	33 11 12	wral	⊢ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒 )
35	34 10 8	wral	⊢ ∀ 𝑥 ∈ 𝑎 ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒 )
36	35 5 9	crab	⊢ { 𝑓 ∈ ( 𝑏 ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒 ) }
37	1 4 3 3 36	cmpo	⊢ ( 𝑎 ∈ 𝒫 ℂ , 𝑏 ∈ 𝒫 ℂ ↦ { 𝑓 ∈ ( 𝑏 ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒 ) } )
38	0 37	wceq	⊢ –cn→ = ( 𝑎 ∈ 𝒫 ℂ , 𝑏 ∈ 𝒫 ℂ ↦ { 𝑓 ∈ ( 𝑏 ↑m 𝑎 ) ∣ ∀ 𝑥 ∈ 𝑎 ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑎 ( ( abs ‘ ( 𝑥 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝑓 ‘ 𝑥 ) − ( 𝑓 ‘ 𝑦 ) ) ) < 𝑒 ) } )