Detailed syntax breakdown of Definition df-mbf
Step | Hyp | Ref
| Expression |
1 | | cmbf 23189 |
. 2
class
MblFn |
2 | | cre 13685 |
. . . . . . . . 9
class
ℜ |
3 | | vf |
. . . . . . . . . 10
setvar 𝑓 |
4 | 3 | cv 1474 |
. . . . . . . . 9
class 𝑓 |
5 | 2, 4 | ccom 5042 |
. . . . . . . 8
class (ℜ
∘ 𝑓) |
6 | 5 | ccnv 5037 |
. . . . . . 7
class ◡(ℜ ∘ 𝑓) |
7 | | vx |
. . . . . . . 8
setvar 𝑥 |
8 | 7 | cv 1474 |
. . . . . . 7
class 𝑥 |
9 | 6, 8 | cima 5041 |
. . . . . 6
class (◡(ℜ ∘ 𝑓) “ 𝑥) |
10 | | cvol 23039 |
. . . . . . 7
class
vol |
11 | 10 | cdm 5038 |
. . . . . 6
class dom
vol |
12 | 9, 11 | wcel 1977 |
. . . . 5
wff (◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol |
13 | | cim 13686 |
. . . . . . . . 9
class
ℑ |
14 | 13, 4 | ccom 5042 |
. . . . . . . 8
class (ℑ
∘ 𝑓) |
15 | 14 | ccnv 5037 |
. . . . . . 7
class ◡(ℑ ∘ 𝑓) |
16 | 15, 8 | cima 5041 |
. . . . . 6
class (◡(ℑ ∘ 𝑓) “ 𝑥) |
17 | 16, 11 | wcel 1977 |
. . . . 5
wff (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol |
18 | 12, 17 | wa 383 |
. . . 4
wff ((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol) |
19 | | cioo 12046 |
. . . . 5
class
(,) |
20 | 19 | crn 5039 |
. . . 4
class ran
(,) |
21 | 18, 7, 20 | wral 2896 |
. . 3
wff
∀𝑥 ∈ ran
(,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol) |
22 | | cc 9813 |
. . . 4
class
ℂ |
23 | | cr 9814 |
. . . 4
class
ℝ |
24 | | cpm 7745 |
. . . 4
class
↑pm |
25 | 22, 23, 24 | co 6549 |
. . 3
class (ℂ
↑pm ℝ) |
26 | 21, 3, 25 | crab 2900 |
. 2
class {𝑓 ∈ (ℂ
↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)} |
27 | 1, 26 | wceq 1475 |
1
wff MblFn =
{𝑓 ∈ (ℂ
↑pm ℝ) ∣ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝑓) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝑓) “ 𝑥) ∈ dom vol)} |