Detailed syntax breakdown of Definition df-homf
Step | Hyp | Ref
| Expression |
1 | | chomf 16980 |
. 2
class
Homf |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | cvv 3407 |
. . 3
class
V |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | | vy |
. . . 4
setvar 𝑦 |
6 | 2 | cv 1538 |
. . . . 5
class 𝑐 |
7 | | cbs 16526 |
. . . . 5
class
Base |
8 | 6, 7 | cfv 6328 |
. . . 4
class
(Base‘𝑐) |
9 | 4 | cv 1538 |
. . . . 5
class 𝑥 |
10 | 5 | cv 1538 |
. . . . 5
class 𝑦 |
11 | | chom 16619 |
. . . . . 6
class
Hom |
12 | 6, 11 | cfv 6328 |
. . . . 5
class (Hom
‘𝑐) |
13 | 9, 10, 12 | co 7143 |
. . . 4
class (𝑥(Hom ‘𝑐)𝑦) |
14 | 4, 5, 8, 8, 13 | cmpo 7145 |
. . 3
class (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦)) |
15 | 2, 3, 14 | cmpt 5105 |
. 2
class (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦))) |
16 | 1, 15 | wceq 1539 |
1
wff
Homf = (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦))) |