This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-cncf

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

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

Detailed syntax breakdown

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