Theorem hof2

Description: The morphism part of the Hom functor, for morphisms <. f , g >. : <. X , Y >. --> <. Z , W >. (which since the first argument is contravariant means morphisms f : Z --> X and g : Y --> W ), yields a function (a morphism of SetCat ) mapping h : X --> Y to g o. h o. f : Z --> W . (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	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	hof2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
	hof2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
	hof2.o	⊢ · = ( comp ‘ 𝐶 )
	hof2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑍 𝐻 𝑋 ) )
	hof2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑊 ) )
	hof2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion	hof2	⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐺 ) ‘ 𝐾 ) = ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐾 ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) )

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		hof2.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8		hof2.w	⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
9		hof2.o	⊢ · = ( comp ‘ 𝐶 )
10		hof2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑍 𝐻 𝑋 ) )
11		hof2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐻 𝑊 ) )
12		hof2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐻 𝑌 ) )
13	1 2 3 4 5 6 7 8 9 10 11	hof2val	⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐺 ) = ( ℎ ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) ) )
14		simpr	⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ℎ = 𝐾 )
15	14	oveq2d	⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) = ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐾 ) )
16	15	oveq1d	⊢ ( ( 𝜑 ∧ ℎ = 𝐾 ) → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) ℎ ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) = ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐾 ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) )
17		ovexd	⊢ ( 𝜑 → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐾 ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) ∈ V )
18	13 16 12 17	fvmptd	⊢ ( 𝜑 → ( ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ ( 2nd ‘ 𝑀 ) ⟨ 𝑍 , 𝑊 ⟩ ) 𝐺 ) ‘ 𝐾 ) = ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑊 ) 𝐾 ) ( ⟨ 𝑍 , 𝑋 ⟩ · 𝑊 ) 𝐹 ) )