Definition df-cncf 25161

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 25159	. 2 class –cn→
2		va	. . 3 setvar 𝑎
3		vb	. . 3 setvar 𝑏
4		cc 11170	. . . 4 class ℂ
5	4	cpw 4556	. . 3 class 𝒫 ℂ
6		vx	. . . . . . . . . . . . 13 setvar 𝑥
7	6	cv 1569	. . . . . . . . . . . 12 class 𝑥
8		vy	. . . . . . . . . . . . 13 setvar 𝑦
9	8	cv 1569	. . . . . . . . . . . 12 class 𝑦
10		cmin 11513	. . . . . . . . . . . 12 class −
11	7, 9, 10	co 7408	. . . . . . . . . . 11 class (𝑥 − 𝑦)
12		cabs 15369	. . . . . . . . . . 11 class abs
13	11, 12	cfv 6527	. . . . . . . . . 10 class (abs‘(𝑥 − 𝑦))
14		vd	. . . . . . . . . . 11 setvar 𝑑
15	14	cv 1569	. . . . . . . . . 10 class 𝑑
16		clt 11315	. . . . . . . . . 10 class <
17	13, 15, 16	wbr 5102	. . . . . . . . 9 wff (abs‘(𝑥 − 𝑦)) < 𝑑
18		vf	. . . . . . . . . . . . . 14 setvar 𝑓
19	18	cv 1569	. . . . . . . . . . . . 13 class 𝑓
20	7, 19	cfv 6527	. . . . . . . . . . . 12 class (𝑓‘𝑥)
21	9, 19	cfv 6527	. . . . . . . . . . . 12 class (𝑓‘𝑦)
22	20, 21, 10	co 7408	. . . . . . . . . . 11 class ((𝑓‘𝑥) − (𝑓‘𝑦))
23	22, 12	cfv 6527	. . . . . . . . . 10 class (abs‘((𝑓‘𝑥) − (𝑓‘𝑦)))
24		ve	. . . . . . . . . . 11 setvar 𝑒
25	24	cv 1569	. . . . . . . . . 10 class 𝑒
26	23, 25, 16	wbr 5102	. . . . . . . . 9 wff (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒
27	17, 26	wi 4	. . . . . . . 8 wff ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)
28	2	cv 1569	. . . . . . . 8 class 𝑎
29	27, 8, 28	wral 3076	. . . . . . 7 wff ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)
30		crp 13090	. . . . . . 7 class ℝ+
31	29, 14, 30	wrex 3086	. . . . . 6 wff ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)
32	31, 24, 30	wral 3076	. . . . 5 wff ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)
33	32, 6, 28	wral 3076	. . . 4 wff ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)
34	3	cv 1569	. . . . 5 class 𝑏
35		cmap 8825	. . . . 5 class ↑m
36	34, 28, 35	co 7408	. . . 4 class (𝑏 ↑m 𝑎)
37	33, 18, 36	crab 3412	. . 3 class {𝑓 ∈ (𝑏 ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)}
38	2, 3, 5, 5, 37	cmpo 7410	. 2 class (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)})
39	1, 38	wceq 1570	1 wff –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)})

This definition is used by:  cncfval  25171  cncfrss  25174  cncfrss2  25175