Theorem fnfuc

Description: The FuncCat operation is a well-defined function on categories. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Assertion	fnfuc	|- FuncCat Fn ( Cat X. Cat )

Proof

Step	Hyp	Ref	Expression
1		df-fuc	|- FuncCat = ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )
2		tpex	|- { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } e. _V
3	1 2	fnmpoi	|- FuncCat Fn ( Cat X. Cat )