Theorem comffn

Description: The functionalized composition operation is a function. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	comfffn.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
	comfffn.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	comffn.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	comffn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	comffn.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	comffn.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
Assertion	comffn	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) Fn ( ( 𝑌 𝐻 𝑍 ) × ( 𝑋 𝐻 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		comfffn.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
2		comfffn.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		comffn.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		comffn.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		comffn.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		comffn.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
7		eqid	⊢ ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑓 ) ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑓 ) )
8		ovex	⊢ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑓 ) ∈ V
9	7 8	fnmpoi	⊢ ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑓 ) ) Fn ( ( 𝑌 𝐻 𝑍 ) × ( 𝑋 𝐻 𝑌 ) )
10		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11	1 2 3 10 4 5 6	comffval	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) = ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑓 ) ) )
12	11	fneq1d	⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) Fn ( ( 𝑌 𝐻 𝑍 ) × ( 𝑋 𝐻 𝑌 ) ) ↔ ( 𝑔 ∈ ( 𝑌 𝐻 𝑍 ) , 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑍 ) 𝑓 ) ) Fn ( ( 𝑌 𝐻 𝑍 ) × ( 𝑋 𝐻 𝑌 ) ) ) )
13	9 12	mpbiri	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑂 𝑍 ) Fn ( ( 𝑌 𝐻 𝑍 ) × ( 𝑋 𝐻 𝑌 ) ) )