Theorem fucoisfunc

Description: A characterization of functors with the object part of functor composition, in terms of an exact morphism function and compatible component functors. See fucoisfunc2 for the componentwise form. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	fucoisfunc.w	$$⊢W=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
	fucoisfunc.t	$$⊢T=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
	fucoisfunc.q	$$⊢Q=C\mathrm{FuncCat}E$$
	fucoisfunc.o	$$⊢O={{\circ }_{\mathrm{func}}\upharpoonright }_W$$
	fucoisfunc.h	$$⊢H=\mathrm{Hom}\left(T\right)$$
	fucoisfunc.i	$$⊢I=\mathrm{Id}\left(T\right)$$
	fucoisfunc.j	$$⊢J=\mathrm{Id}\left(Q\right)$$
	fucoisfunc.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(T\right)$$
	fucoisfunc.y	No typesetting found for |- .o. = ( comp ` Q ) with typecode |-
	fucoisfunc.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	fucoisfunc.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	fucoisfunc.e	$$⊢\phi \to E\in \mathrm{Cat}$$
Assertion	fucoisfunc	Could not format assertion : No typesetting found for |- ( ph -> ( O ( T Func Q ) P <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fucoisfunc.w	$$⊢W=\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)$$
2		fucoisfunc.t	$$⊢T=\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)$$
3		fucoisfunc.q	$$⊢Q=C\mathrm{FuncCat}E$$
4		fucoisfunc.o	$$⊢O={{\circ }_{\mathrm{func}}\upharpoonright }_W$$
5		fucoisfunc.h	$$⊢H=\mathrm{Hom}\left(T\right)$$
6		fucoisfunc.i	$$⊢I=\mathrm{Id}\left(T\right)$$
7		fucoisfunc.j	$$⊢J=\mathrm{Id}\left(Q\right)$$
8		fucoisfunc.x	$$⊢\underset{\dot{}}{·}=\mathrm{comp}\left(T\right)$$
9		fucoisfunc.y	Could not format .o. = ( comp ` Q ) : No typesetting found for |- .o. = ( comp ` Q ) with typecode |-
10		fucoisfunc.c	$$⊢\phi \to C\in \mathrm{Cat}$$
11		fucoisfunc.d	$$⊢\phi \to D\in \mathrm{Cat}$$
12		fucoisfunc.e	$$⊢\phi \to E\in \mathrm{Cat}$$
13	2	xpcfucbas	$$⊢\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)={\mathrm{Base}}_T$$
14	1 13	eqtri	$$⊢W={\mathrm{Base}}_T$$
15	3	fucbas	$$⊢C\mathrm{Func}E={\mathrm{Base}}_Q$$
16		eqid	$$⊢C\mathrm{Nat}E=C\mathrm{Nat}E$$
17	3 16	fuchom	$$⊢C\mathrm{Nat}E=\mathrm{Hom}\left(Q\right)$$
18		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
19	18 11 12	fuccat	$$⊢\phi \to D\mathrm{FuncCat}E\in \mathrm{Cat}$$
20		eqid	$$⊢C\mathrm{FuncCat}D=C\mathrm{FuncCat}D$$
21	20 10 11	fuccat	$$⊢\phi \to C\mathrm{FuncCat}D\in \mathrm{Cat}$$
22	2 19 21	xpccat	$$⊢\phi \to T\in \mathrm{Cat}$$
23	3 10 12	fuccat	$$⊢\phi \to Q\in \mathrm{Cat}$$
24	14 15 5 17 6 7 8 9 22 23	isfunc	Could not format ( ph -> ( O ( T Func Q ) P <-> ( O : W --> ( C Func E ) /\ P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( O ( T Func Q ) P <-> ( O : W --> ( C Func E ) /\ P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) with typecode |-
25		rescofuf	$$⊢\left({{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}\right):\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)⟶C\mathrm{Func}E$$
26	1	reseq2i	$$⊢{{\circ }_{\mathrm{func}}\upharpoonright }_W={{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}$$
27	4 26	eqtri	$$⊢O={{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}$$
28	27 1	feq12i	$$⊢O:W⟶C\mathrm{Func}E\leftrightarrow \left({{\circ }_{\mathrm{func}}\upharpoonright }_{\left(\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)\right)}\right):\left(D\mathrm{Func}E\right)\times \left(C\mathrm{Func}D\right)⟶C\mathrm{Func}E$$
29	25 28	mpbir	$$⊢O:W⟶C\mathrm{Func}E$$
30		3anass	Could not format ( ( O : W --> ( C Func E ) /\ P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( O : W --> ( C Func E ) /\ ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) : No typesetting found for |- ( ( O : W --> ( C Func E ) /\ P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( O : W --> ( C Func E ) /\ ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) with typecode |-
31	29 30	mpbiran	Could not format ( ( O : W --> ( C Func E ) /\ P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) : No typesetting found for |- ( ( O : W --> ( C Func E ) /\ P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) with typecode |-
32	24 31	bitrdi	Could not format ( ph -> ( O ( T Func Q ) P <-> ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( O ( T Func Q ) P <-> ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) with typecode |-
33	2	fveq2i	$$⊢\mathrm{Hom}\left(T\right)=\mathrm{Hom}\left(\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)\right)$$
34	5 33	eqtri	$$⊢H=\mathrm{Hom}\left(\left(D\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}D\right)\right)$$
35	1 34	fucofulem2	$$⊢P\in \underset{z\in W\times W}{⨉}\left({\left(O\left(1^{st}\left(z\right)\right)\left(C\mathrm{Nat}E\right)O\left(2^{nd}\left(z\right)\right)\right)}^{H\left(z\right)}\right)\leftrightarrow \left(P=\left(u\in W,v\in W⟼uPv\right)\wedge \forall m\in W\forall n\in W\left(mPn=\left(b\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right),a\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)⟼b\left(mPn\right)a\right)\wedge \forall p\in \left(1^{st}\left(m\right)\left(D\mathrm{Nat}E\right)1^{st}\left(n\right)\right)\forall q\in \left(2^{nd}\left(m\right)\left(C\mathrm{Nat}D\right)2^{nd}\left(n\right)\right)p\left(mPn\right)q\in \left(O\left(m\right)\left(C\mathrm{Nat}E\right)O\left(n\right)\right)\right)\right)$$
36	35	anbi1i	Could not format ( ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) : No typesetting found for |- ( ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) with typecode |-
37	32 36	bitrdi	Could not format ( ph -> ( O ( T Func Q ) P <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( O ( T Func Q ) P <-> ( ( P = ( u e. W , v e. W |-> ( u P v ) ) /\ A. m e. W A. n e. W ( ( m P n ) = ( b e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) , a e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) |-> ( b ( m P n ) a ) ) /\ A. p e. ( ( 1st ` m ) ( D Nat E ) ( 1st ` n ) ) A. q e. ( ( 2nd ` m ) ( C Nat D ) ( 2nd ` n ) ) ( p ( m P n ) q ) e. ( ( O ` m ) ( C Nat E ) ( O ` n ) ) ) ) /\ A. x e. W ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. .o. ( O ` z ) ) ( ( x P y ) ` m ) ) ) ) ) ) with typecode |-