Theorem hof1

Description: The object part of the Hom functor maps X , Y to the set of morphisms from X to Y . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	⊢ 𝑀 = ( HomF ‘ 𝐶 )
	hofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	hof1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	hof1.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	hof1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	hof1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	hof1	⊢ ( 𝜑 → ( 𝑋 ( 1st ‘ 𝑀 ) 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		hofval.m	⊢ 𝑀 = ( HomF ‘ 𝐶 )
2		hofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		hof1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		hof1.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
5		hof1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		hof1.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7	1 2	hof1fval	⊢ ( 𝜑 → ( 1st ‘ 𝑀 ) = ( Homf ‘ 𝐶 ) )
8	7	oveqd	⊢ ( 𝜑 → ( 𝑋 ( 1st ‘ 𝑀 ) 𝑌 ) = ( 𝑋 ( Homf ‘ 𝐶 ) 𝑌 ) )
9		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
10	9 3 4 5 6	homfval	⊢ ( 𝜑 → ( 𝑋 ( Homf ‘ 𝐶 ) 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )
11	8 10	eqtrd	⊢ ( 𝜑 → ( 𝑋 ( 1st ‘ 𝑀 ) 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )