Theorem fucofunc

Description: The functor composition bifunctor is a functor. See also fucofunca .

Its object function need not determine its morphism function; see fuconuniqex2 . In fuconuniqex both source categories are ( SetCat1o ) . The witness target is the category of par2cat , with two objects and two parallel nonidentity arrows. The map in fuconuniq exchanges those arrows and gives another functor with exactly the same object function; fuconuniq2 states its existence. At a natural-transformation/identity pair, the canonical and alternative components are respectively (/) and 1o , as proved in fuconuniqvals .

For arbitrary categories, fucoisfunc characterizes all morphism parts with the object function ` ( o.func |`W ) of functor composition. The componentwise version fucoisfunc2 expresses the three exact function domains suggested by df-fuco and fuco23 , together with component typing, naturality, and the identity and composition laws. These conditions allow component values other than those of the canonical construction.

(Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fucoco2.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
	fucoco2.q	|- Q = ( C FuncCat E )
	fucoco2.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
	fucofunc.c	|- ( ph -> C e. Cat )
	fucofunc.d	|- ( ph -> D e. Cat )
	fucofunc.e	|- ( ph -> E e. Cat )
Assertion	fucofunc	|- ( ph -> O ( T Func Q ) P )

Proof

Step	Hyp	Ref	Expression
1		fucoco2.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
2		fucoco2.q	|- Q = ( C FuncCat E )
3		fucoco2.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
4		fucofunc.c	|- ( ph -> C e. Cat )
5		fucofunc.d	|- ( ph -> D e. Cat )
6		fucofunc.e	|- ( ph -> E e. Cat )
7	1	xpcfucbas	|- ( ( D Func E ) X. ( C Func D ) ) = ( Base ` T )
8	2	fucbas	|- ( C Func E ) = ( Base ` Q )
9		eqid	|- ( Hom ` T ) = ( Hom ` T )
10		eqid	|- ( C Nat E ) = ( C Nat E )
11	2 10	fuchom	|- ( C Nat E ) = ( Hom ` Q )
12		eqid	|- ( Id ` T ) = ( Id ` T )
13		eqid	|- ( Id ` Q ) = ( Id ` Q )
14		eqid	|- ( comp ` T ) = ( comp ` T )
15		eqid	|- ( comp ` Q ) = ( comp ` Q )
16		eqid	|- ( D FuncCat E ) = ( D FuncCat E )
17	16 5 6	fuccat	|- ( ph -> ( D FuncCat E ) e. Cat )
18		eqid	|- ( C FuncCat D ) = ( C FuncCat D )
19	18 4 5	fuccat	|- ( ph -> ( C FuncCat D ) e. Cat )
20	1 17 19	xpccat	|- ( ph -> T e. Cat )
21	2 4 6	fuccat	|- ( ph -> Q e. Cat )
22		eqidd	|- ( ph -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
23	4 5 6 3 22	fucof1	|- ( ph -> O : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E ) )
24	4 5 6 3 22	fucofn2	|- ( ph -> P Fn ( ( ( D Func E ) X. ( C Func D ) ) X. ( ( D Func E ) X. ( C Func D ) ) ) )
25	3	adantr	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. )
26		eqidd	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
27		simprl	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> x e. ( ( D Func E ) X. ( C Func D ) ) )
28		simprr	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> y e. ( ( D Func E ) X. ( C Func D ) ) )
29	25 1 9 26 27 28	fucof21	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> ( x P y ) : ( x ( Hom ` T ) y ) --> ( ( O ` x ) ( C Nat E ) ( O ` y ) ) )
30	3	adantr	|- ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. )
31		eqidd	|- ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
32		simpr	|- ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> x e. ( ( D Func E ) X. ( C Func D ) ) )
33	30 1 12 2 13 31 32	fucoid2	|- ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> ( ( x P x ) ` ( ( Id ` T ) ` x ) ) = ( ( Id ` Q ) ` ( O ` x ) ) )
34	3	3ad2ant1	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. )
35		eqidd	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
36		simp21	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> x e. ( ( D Func E ) X. ( C Func D ) ) )
37		simp22	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> y e. ( ( D Func E ) X. ( C Func D ) ) )
38		simp23	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> z e. ( ( D Func E ) X. ( C Func D ) ) )
39		simp3l	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> m e. ( x ( Hom ` T ) y ) )
40		simp3r	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> n e. ( y ( Hom ` T ) z ) )
41	1 2 34 14 15 35 36 37 38 9 39 40	fucoco2	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> ( ( x P z ) ` ( n ( <. x , y >. ( comp ` T ) z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. ( comp ` Q ) ( O ` z ) ) ( ( x P y ) ` m ) ) )
42	7 8 9 11 12 13 14 15 20 21 23 24 29 33 41	isfuncd	|- ( ph -> O ( T Func Q ) P )