Detailed syntax breakdown of Definition df-cau
Step | Hyp | Ref
| Expression |
1 | | ccau 24150 |
. 2
class
Cau |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cxmet 20348 |
. . . . 5
class
∞Met |
4 | 3 | crn 5552 |
. . . 4
class ran
∞Met |
5 | 4 | cuni 4819 |
. . 3
class ∪ ran ∞Met |
6 | | vj |
. . . . . . . . 9
setvar 𝑗 |
7 | 6 | cv 1542 |
. . . . . . . 8
class 𝑗 |
8 | | cuz 12438 |
. . . . . . . 8
class
ℤ≥ |
9 | 7, 8 | cfv 6380 |
. . . . . . 7
class
(ℤ≥‘𝑗) |
10 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
11 | 10 | cv 1542 |
. . . . . . . . 9
class 𝑓 |
12 | 7, 11 | cfv 6380 |
. . . . . . . 8
class (𝑓‘𝑗) |
13 | | vx |
. . . . . . . . 9
setvar 𝑥 |
14 | 13 | cv 1542 |
. . . . . . . 8
class 𝑥 |
15 | 2 | cv 1542 |
. . . . . . . . 9
class 𝑑 |
16 | | cbl 20350 |
. . . . . . . . 9
class
ball |
17 | 15, 16 | cfv 6380 |
. . . . . . . 8
class
(ball‘𝑑) |
18 | 12, 14, 17 | co 7213 |
. . . . . . 7
class ((𝑓‘𝑗)(ball‘𝑑)𝑥) |
19 | 11, 9 | cres 5553 |
. . . . . . 7
class (𝑓 ↾
(ℤ≥‘𝑗)) |
20 | 9, 18, 19 | wf 6376 |
. . . . . 6
wff (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥) |
21 | | cz 12176 |
. . . . . 6
class
ℤ |
22 | 20, 6, 21 | wrex 3062 |
. . . . 5
wff
∃𝑗 ∈
ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥) |
23 | | crp 12586 |
. . . . 5
class
ℝ+ |
24 | 22, 13, 23 | wral 3061 |
. . . 4
wff
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥) |
25 | 15 | cdm 5551 |
. . . . . 6
class dom 𝑑 |
26 | 25 | cdm 5551 |
. . . . 5
class dom dom
𝑑 |
27 | | cc 10727 |
. . . . 5
class
ℂ |
28 | | cpm 8509 |
. . . . 5
class
↑pm |
29 | 26, 27, 28 | co 7213 |
. . . 4
class (dom dom
𝑑 ↑pm
ℂ) |
30 | 24, 10, 29 | crab 3065 |
. . 3
class {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ)
∣ ∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)} |
31 | 2, 5, 30 | cmpt 5135 |
. 2
class (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)}) |
32 | 1, 31 | wceq 1543 |
1
wff Cau =
(𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)}) |