# Metamath Proof Explorer

## Definition df-homf

Description: Define the functionalized Hom-set operator, which is exactly like Hom but is guaranteed to be a function on the base. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Assertion df-homf ${⊢}{\mathrm{Hom}}_{𝑓}=\left({c}\in \mathrm{V}⟼\left({x}\in {\mathrm{Base}}_{{c}},{y}\in {\mathrm{Base}}_{{c}}⟼{x}\mathrm{Hom}\left({c}\right){y}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chomf ${class}{\mathrm{Hom}}_{𝑓}$
1 vc ${setvar}{c}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{c}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{c}}$
7 vy ${setvar}{y}$
8 3 cv ${setvar}{x}$
9 chom ${class}\mathrm{Hom}$
10 5 9 cfv ${class}\mathrm{Hom}\left({c}\right)$
11 7 cv ${setvar}{y}$
12 8 11 10 co ${class}\left({x}\mathrm{Hom}\left({c}\right){y}\right)$
13 3 7 6 6 12 cmpo ${class}\left({x}\in {\mathrm{Base}}_{{c}},{y}\in {\mathrm{Base}}_{{c}}⟼{x}\mathrm{Hom}\left({c}\right){y}\right)$
14 1 2 13 cmpt ${class}\left({c}\in \mathrm{V}⟼\left({x}\in {\mathrm{Base}}_{{c}},{y}\in {\mathrm{Base}}_{{c}}⟼{x}\mathrm{Hom}\left({c}\right){y}\right)\right)$
15 0 14 wceq ${wff}{\mathrm{Hom}}_{𝑓}=\left({c}\in \mathrm{V}⟼\left({x}\in {\mathrm{Base}}_{{c}},{y}\in {\mathrm{Base}}_{{c}}⟼{x}\mathrm{Hom}\left({c}\right){y}\right)\right)$