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 Hom 𝑓 = c V x Base c , y Base c x Hom c y

Detailed syntax breakdown

Step Hyp Ref Expression
0 chomf class Hom 𝑓
1 vc setvar c
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar c
6 5 4 cfv class Base c
7 vy setvar y
8 3 cv setvar x
9 chom class Hom
10 5 9 cfv class Hom c
11 7 cv setvar y
12 8 11 10 co class x Hom c y
13 3 7 6 6 12 cmpo class x Base c , y Base c x Hom c y
14 1 2 13 cmpt class c V x Base c , y Base c x Hom c y
15 0 14 wceq wff Hom 𝑓 = c V x Base c , y Base c x Hom c y