Definition df-cncf 23947

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

Assertion

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

Distinct variable group:   𝑎,𝑏,𝑑,𝑒,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-cncf

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

This definition is referenced by:  cncfval  23957  cncfrss  23960  cncfrss2  23961