Theorem fucoisfunc2

Description: Full componentwise characterization of an arbitrary morphism part with the object function of functor composition. See also fucoisfunc .

Its three exact function domains, component types and naturality, and pointwise identity and composition laws are necessary and sufficient. Empty object and hom domains are permitted. For a concrete failure of uniqueness, see fuconuniq and fuconuniqex2 . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	fucoisfunc.w	|- W = ( ( D Func E ) X. ( C Func D ) )
	fucoisfunc2lem1.o	|- O = ( o.func |` W )
	fucoisfunc2lem1.b	|- B = ( Base ` C )
	fucoisfunc2lem1.r	|- R = ( Hom ` C )
	fucoisfunc2lem1.s	|- S = ( Hom ` E )
	fucoisfunc2lem1.v	|- .xb = ( comp ` E )
	fucoisfunc2.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
	fucoisfunc2.q	|- Q = ( C FuncCat E )
	fucoisfunc2.h	|- H = ( Hom ` T )
	fucoisfunc2.i	|- I = ( Id ` T )
	fucoisfunc2.x	|- .x. = ( comp ` T )
	fucoisfunc2.c	|- ( ph -> C e. Cat )
	fucoisfunc2.d	|- ( ph -> D e. Cat )
	fucoisfunc2.e	|- ( ph -> E e. Cat )
	fucoisfunc2.k	|- K = ( Id ` E )
Assertion	fucoisfunc2	|- ( 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 ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoisfunc.w	|- W = ( ( D Func E ) X. ( C Func D ) )
2		fucoisfunc2lem1.o	|- O = ( o.func |` W )
3		fucoisfunc2lem1.b	|- B = ( Base ` C )
4		fucoisfunc2lem1.r	|- R = ( Hom ` C )
5		fucoisfunc2lem1.s	|- S = ( Hom ` E )
6		fucoisfunc2lem1.v	|- .xb = ( comp ` E )
7		fucoisfunc2.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
8		fucoisfunc2.q	|- Q = ( C FuncCat E )
9		fucoisfunc2.h	|- H = ( Hom ` T )
10		fucoisfunc2.i	|- I = ( Id ` T )
11		fucoisfunc2.x	|- .x. = ( comp ` T )
12		fucoisfunc2.c	|- ( ph -> C e. Cat )
13		fucoisfunc2.d	|- ( ph -> D e. Cat )
14		fucoisfunc2.e	|- ( ph -> E e. Cat )
15		fucoisfunc2.k	|- K = ( Id ` E )
16		eqid	|- ( Id ` Q ) = ( Id ` Q )
17		eqid	|- ( comp ` Q ) = ( comp ` Q )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	fucoisfunc2lem2	|- ( 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 ) = ( x e. B |-> ( ( p ( m P n ) q ) ` x ) ) /\ A. x e. B ( ( p ( m P n ) q ) ` x ) e. ( ( ( 1st ` ( O ` m ) ) ` x ) S ( ( 1st ` ( O ` n ) ) ` x ) ) /\ A. x e. B A. y e. B A. h e. ( x R y ) ( ( ( p ( m P n ) q ) ` y ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` m ) ) ` y ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( x ( 2nd ` ( O ` m ) ) y ) ` h ) ) = ( ( ( x ( 2nd ` ( O ` n ) ) y ) ` h ) ( <. ( ( 1st ` ( O ` m ) ) ` x ) , ( ( 1st ` ( O ` n ) ) ` x ) >. .xb ( ( 1st ` ( O ` n ) ) ` y ) ) ( ( p ( m P n ) q ) ` x ) ) ) ) ) /\ A. x e. W ( A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) /\ A. y e. W A. z e. W A. m e. ( x H y ) A. n e. ( y H z ) A. t e. B ( ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) ` t ) = ( ( ( ( y P z ) ` n ) ` t ) ( <. ( ( 1st ` ( O ` x ) ) ` t ) , ( ( 1st ` ( O ` y ) ) ` t ) >. .xb ( ( 1st ` ( O ` z ) ) ` t ) ) ( ( ( x P y ) ` m ) ` t ) ) ) ) ) )