Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cncf Structured version   Visualization version   GIF version

Definition df-cncf 23051
 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→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
Distinct variable group:   𝑎,𝑏,𝑑,𝑒,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-cncf
StepHypRef Expression
1 ccncf 23049 . 2 class cn
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 cc 10250 . . . 4 class
54cpw 4378 . . 3 class 𝒫 ℂ
6 vx . . . . . . . . . . . . 13 setvar 𝑥
76cv 1657 . . . . . . . . . . . 12 class 𝑥
8 vy . . . . . . . . . . . . 13 setvar 𝑦
98cv 1657 . . . . . . . . . . . 12 class 𝑦
10 cmin 10585 . . . . . . . . . . . 12 class
117, 9, 10co 6905 . . . . . . . . . . 11 class (𝑥𝑦)
12 cabs 14351 . . . . . . . . . . 11 class abs
1311, 12cfv 6123 . . . . . . . . . 10 class (abs‘(𝑥𝑦))
14 vd . . . . . . . . . . 11 setvar 𝑑
1514cv 1657 . . . . . . . . . 10 class 𝑑
16 clt 10391 . . . . . . . . . 10 class <
1713, 15, 16wbr 4873 . . . . . . . . 9 wff (abs‘(𝑥𝑦)) < 𝑑
18 vf . . . . . . . . . . . . . 14 setvar 𝑓
1918cv 1657 . . . . . . . . . . . . 13 class 𝑓
207, 19cfv 6123 . . . . . . . . . . . 12 class (𝑓𝑥)
219, 19cfv 6123 . . . . . . . . . . . 12 class (𝑓𝑦)
2220, 21, 10co 6905 . . . . . . . . . . 11 class ((𝑓𝑥) − (𝑓𝑦))
2322, 12cfv 6123 . . . . . . . . . 10 class (abs‘((𝑓𝑥) − (𝑓𝑦)))
24 ve . . . . . . . . . . 11 setvar 𝑒
2524cv 1657 . . . . . . . . . 10 class 𝑒
2623, 25, 16wbr 4873 . . . . . . . . 9 wff (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒
2717, 26wi 4 . . . . . . . 8 wff ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
282cv 1657 . . . . . . . 8 class 𝑎
2927, 8, 28wral 3117 . . . . . . 7 wff 𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
30 crp 12112 . . . . . . 7 class +
3129, 14, 30wrex 3118 . . . . . 6 wff 𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
3231, 24, 30wral 3117 . . . . 5 wff 𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
3332, 6, 28wral 3117 . . . 4 wff 𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
343cv 1657 . . . . 5 class 𝑏
35 cmap 8122 . . . . 5 class 𝑚
3634, 28, 35co 6905 . . . 4 class (𝑏𝑚 𝑎)
3733, 18, 36crab 3121 . . 3 class {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)}
382, 3, 5, 5, 37cmpt2 6907 . 2 class (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
391, 38wceq 1658 1 wff cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
 Colors of variables: wff setvar class This definition is referenced by:  cncfval  23061  cncfrss  23064  cncfrss2  23065
 Copyright terms: Public domain W3C validator