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

Definition df-cncf 23415
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
StepHypRef Expression
1 ccncf 23413 . 2 class cn
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 cc 10524 . . . 4 class
54cpw 4537 . . 3 class 𝒫 ℂ
6 vx . . . . . . . . . . . . 13 setvar 𝑥
76cv 1527 . . . . . . . . . . . 12 class 𝑥
8 vy . . . . . . . . . . . . 13 setvar 𝑦
98cv 1527 . . . . . . . . . . . 12 class 𝑦
10 cmin 10859 . . . . . . . . . . . 12 class
117, 9, 10co 7145 . . . . . . . . . . 11 class (𝑥𝑦)
12 cabs 14583 . . . . . . . . . . 11 class abs
1311, 12cfv 6349 . . . . . . . . . 10 class (abs‘(𝑥𝑦))
14 vd . . . . . . . . . . 11 setvar 𝑑
1514cv 1527 . . . . . . . . . 10 class 𝑑
16 clt 10664 . . . . . . . . . 10 class <
1713, 15, 16wbr 5058 . . . . . . . . 9 wff (abs‘(𝑥𝑦)) < 𝑑
18 vf . . . . . . . . . . . . . 14 setvar 𝑓
1918cv 1527 . . . . . . . . . . . . 13 class 𝑓
207, 19cfv 6349 . . . . . . . . . . . 12 class (𝑓𝑥)
219, 19cfv 6349 . . . . . . . . . . . 12 class (𝑓𝑦)
2220, 21, 10co 7145 . . . . . . . . . . 11 class ((𝑓𝑥) − (𝑓𝑦))
2322, 12cfv 6349 . . . . . . . . . 10 class (abs‘((𝑓𝑥) − (𝑓𝑦)))
24 ve . . . . . . . . . . 11 setvar 𝑒
2524cv 1527 . . . . . . . . . 10 class 𝑒
2623, 25, 16wbr 5058 . . . . . . . . 9 wff (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒
2717, 26wi 4 . . . . . . . 8 wff ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
282cv 1527 . . . . . . . 8 class 𝑎
2927, 8, 28wral 3138 . . . . . . 7 wff 𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
30 crp 12379 . . . . . . 7 class +
3129, 14, 30wrex 3139 . . . . . 6 wff 𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
3231, 24, 30wral 3138 . . . . 5 wff 𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
3332, 6, 28wral 3138 . . . 4 wff 𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
343cv 1527 . . . . 5 class 𝑏
35 cmap 8396 . . . . 5 class m
3634, 28, 35co 7145 . . . 4 class (𝑏m 𝑎)
3733, 18, 36crab 3142 . . 3 class {𝑓 ∈ (𝑏m 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)}
382, 3, 5, 5, 37cmpo 7147 . 2 class (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏m 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
391, 38wceq 1528 1 wff cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏m 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
Colors of variables: wff setvar class
This definition is referenced by:  cncfval  23425  cncfrss  23428  cncfrss2  23429
  Copyright terms: Public domain W3C validator