Detailed syntax breakdown of Definition df-homf
Step | Hyp | Ref
| Expression |
1 | | chomf 17169 |
. 2
class
Homf |
2 | | vc |
. . 3
setvar 𝑐 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vx |
. . . 4
setvar 𝑥 |
5 | | vy |
. . . 4
setvar 𝑦 |
6 | 2 | cv 1542 |
. . . . 5
class 𝑐 |
7 | | cbs 16760 |
. . . . 5
class
Base |
8 | 6, 7 | cfv 6380 |
. . . 4
class
(Base‘𝑐) |
9 | 4 | cv 1542 |
. . . . 5
class 𝑥 |
10 | 5 | cv 1542 |
. . . . 5
class 𝑦 |
11 | | chom 16813 |
. . . . . 6
class
Hom |
12 | 6, 11 | cfv 6380 |
. . . . 5
class (Hom
‘𝑐) |
13 | 9, 10, 12 | co 7213 |
. . . 4
class (𝑥(Hom ‘𝑐)𝑦) |
14 | 4, 5, 8, 8, 13 | cmpo 7215 |
. . 3
class (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦)) |
15 | 2, 3, 14 | cmpt 5135 |
. 2
class (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦))) |
16 | 1, 15 | wceq 1543 |
1
wff
Homf = (𝑐 ∈ V ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑥(Hom ‘𝑐)𝑦))) |