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	⊢ Homf = ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chomf	⊢ Homf
1		vc	⊢ 𝑐
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑐
6	5 4	cfv	⊢ ( Base ‘ 𝑐 )
7		vy	⊢ 𝑦
8	3	cv	⊢ 𝑥
9		chom	⊢ Hom
10	5 9	cfv	⊢ ( Hom ‘ 𝑐 )
11	7	cv	⊢ 𝑦
12	8 11 10	co	⊢ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 )
13	3 7 6 6 12	cmpo	⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) )
14	1 2 13	cmpt	⊢ ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ) )
15	0 14	wceq	⊢ Homf = ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑦 ) ) )