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 22417
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 22415 . 2 class cn
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 cc 9787 . . . 4 class
54cpw 4104 . . 3 class 𝒫 ℂ
6 vx . . . . . . . . . . . . 13 setvar 𝑥
76cv 1473 . . . . . . . . . . . 12 class 𝑥
8 vy . . . . . . . . . . . . 13 setvar 𝑦
98cv 1473 . . . . . . . . . . . 12 class 𝑦
10 cmin 10114 . . . . . . . . . . . 12 class
117, 9, 10co 6524 . . . . . . . . . . 11 class (𝑥𝑦)
12 cabs 13765 . . . . . . . . . . 11 class abs
1311, 12cfv 5787 . . . . . . . . . 10 class (abs‘(𝑥𝑦))
14 vd . . . . . . . . . . 11 setvar 𝑑
1514cv 1473 . . . . . . . . . 10 class 𝑑
16 clt 9927 . . . . . . . . . 10 class <
1713, 15, 16wbr 4574 . . . . . . . . 9 wff (abs‘(𝑥𝑦)) < 𝑑
18 vf . . . . . . . . . . . . . 14 setvar 𝑓
1918cv 1473 . . . . . . . . . . . . 13 class 𝑓
207, 19cfv 5787 . . . . . . . . . . . 12 class (𝑓𝑥)
219, 19cfv 5787 . . . . . . . . . . . 12 class (𝑓𝑦)
2220, 21, 10co 6524 . . . . . . . . . . 11 class ((𝑓𝑥) − (𝑓𝑦))
2322, 12cfv 5787 . . . . . . . . . 10 class (abs‘((𝑓𝑥) − (𝑓𝑦)))
24 ve . . . . . . . . . . 11 setvar 𝑒
2524cv 1473 . . . . . . . . . 10 class 𝑒
2623, 25, 16wbr 4574 . . . . . . . . 9 wff (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒
2717, 26wi 4 . . . . . . . 8 wff ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
282cv 1473 . . . . . . . 8 class 𝑎
2927, 8, 28wral 2892 . . . . . . 7 wff 𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
30 crp 11661 . . . . . . 7 class +
3129, 14, 30wrex 2893 . . . . . 6 wff 𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
3231, 24, 30wral 2892 . . . . 5 wff 𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
3332, 6, 28wral 2892 . . . 4 wff 𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
343cv 1473 . . . . 5 class 𝑏
35 cmap 7718 . . . . 5 class 𝑚
3634, 28, 35co 6524 . . . 4 class (𝑏𝑚 𝑎)
3733, 18, 36crab 2896 . . 3 class {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)}
382, 3, 5, 5, 37cmpt2 6526 . 2 class (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
391, 38wceq 1474 1 wff cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
Colors of variables: wff setvar class
This definition is referenced by:  cncfval  22427  cncfrss  22430  cncfrss2  22431
  Copyright terms: Public domain W3C validator