Theorem comfffn

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

	Ref	Expression
Hypotheses	comfffn.o	|- O = ( comf ` C )
	comfffn.b	|- B = ( Base ` C )
Assertion	comfffn	|- O Fn ( ( B X. B ) X. B )

Proof

Step	Hyp	Ref	Expression
1		comfffn.o	|- O = ( comf ` C )
2		comfffn.b	|- B = ( Base ` C )
3		eqid	|- ( Hom ` C ) = ( Hom ` C )
4		eqid	|- ( comp ` C ) = ( comp ` C )
5	1 2 3 4	comfffval	|- O = ( x e. ( B X. B ) , y e. B |-> ( g e. ( ( 2nd ` x ) ( Hom ` C ) y ) , f e. ( ( Hom ` C ) ` x ) |-> ( g ( x ( comp ` C ) y ) f ) ) )
6		ovex	|- ( ( 2nd ` x ) ( Hom ` C ) y ) e. _V
7		fvex	|- ( ( Hom ` C ) ` x ) e. _V
8	6 7	mpoex	|- ( g e. ( ( 2nd ` x ) ( Hom ` C ) y ) , f e. ( ( Hom ` C ) ` x ) |-> ( g ( x ( comp ` C ) y ) f ) ) e. _V
9	5 8	fnmpoi	|- O Fn ( ( B X. B ) X. B )