Detailed syntax breakdown of Definition df-fm
| Step | Hyp | Ref
| Expression |
| 1 | | cfm 23941 |
. 2
class
FilMap |
| 2 | | vx |
. . 3
setvar 𝑥 |
| 3 | | vf |
. . 3
setvar 𝑓 |
| 4 | | cvv 3480 |
. . 3
class
V |
| 5 | | vy |
. . . 4
setvar 𝑦 |
| 6 | 3 | cv 1539 |
. . . . . 6
class 𝑓 |
| 7 | 6 | cdm 5685 |
. . . . 5
class dom 𝑓 |
| 8 | | cfbas 21352 |
. . . . 5
class
fBas |
| 9 | 7, 8 | cfv 6561 |
. . . 4
class
(fBas‘dom 𝑓) |
| 10 | 2 | cv 1539 |
. . . . 5
class 𝑥 |
| 11 | | vt |
. . . . . . 7
setvar 𝑡 |
| 12 | 5 | cv 1539 |
. . . . . . 7
class 𝑦 |
| 13 | 11 | cv 1539 |
. . . . . . . 8
class 𝑡 |
| 14 | 6, 13 | cima 5688 |
. . . . . . 7
class (𝑓 “ 𝑡) |
| 15 | 11, 12, 14 | cmpt 5225 |
. . . . . 6
class (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)) |
| 16 | 15 | crn 5686 |
. . . . 5
class ran
(𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)) |
| 17 | | cfg 21353 |
. . . . 5
class
filGen |
| 18 | 10, 16, 17 | co 7431 |
. . . 4
class (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))) |
| 19 | 5, 9, 18 | cmpt 5225 |
. . 3
class (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))) |
| 20 | 2, 3, 4, 4, 19 | cmpo 7433 |
. 2
class (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))))) |
| 21 | 1, 20 | wceq 1540 |
1
wff FilMap =
(𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡))))) |