Theorem comfffn

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

	Ref	Expression
Hypotheses	comfffn.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
	comfffn.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	comfffn	⊢ 𝑂 Fn ( ( 𝐵 × 𝐵 ) × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		comfffn.o	⊢ 𝑂 = ( compf ‘ 𝐶 )
2		comfffn.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
4		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
5	1 2 3 4	comfffval	⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) )
6		ovex	⊢ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) ∈ V
7		fvex	⊢ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ∈ V
8	6 7	mpoex	⊢ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝐶 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝐶 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝐶 ) 𝑦 ) 𝑓 ) ) ∈ V
9	5 8	fnmpoi	⊢ 𝑂 Fn ( ( 𝐵 × 𝐵 ) × 𝐵 )