Metamath Proof Explorer

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 = ( ( D Func E ) X. ( C Func D ) )
fucoisfunc.t 
|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
fucoisfunc.q 
|- Q = ( C FuncCat E )
fucoisfunc.o 
|- O = ( o.func |` W )
fucoisfunc.h 
|- H = ( Hom ` T )
fucoisfunc.i 
|- I = ( Id ` T )
fucoisfunc.j 
|- J = ( Id ` Q )
fucoisfunc.x 
|- .x. = ( comp ` T )
fucoisfunc.y 
|- .o. = ( comp ` Q )
fucoisfunc.c 
|- ( ph -> C e. Cat )
fucoisfunc.d 
|- ( ph -> D e. Cat )
fucoisfunc.e 
|- ( ph -> E e. Cat )
Assertion fucoisfunc 
|- ( 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fucoisfunc.w 
 |-  W = ( ( D Func E ) X. ( C Func D ) )
2 fucoisfunc.t 
 |-  T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
3 fucoisfunc.q 
 |-  Q = ( C FuncCat E )
4 fucoisfunc.o 
 |-  O = ( o.func |` W )
5 fucoisfunc.h 
 |-  H = ( Hom ` T )
6 fucoisfunc.i 
 |-  I = ( Id ` T )
7 fucoisfunc.j 
 |-  J = ( Id ` Q )
8 fucoisfunc.x 
 |-  .x. = ( comp ` T )
9 fucoisfunc.y 
 |-  .o. = ( comp ` Q )
10 fucoisfunc.c 
 |-  ( ph -> C e. Cat )
11 fucoisfunc.d 
 |-  ( ph -> D e. Cat )
12 fucoisfunc.e 
 |-  ( ph -> E e. Cat )
13 2 xpcfucbas 
 |-  ( ( D Func E ) X. ( C Func D ) ) = ( Base ` T )
14 1 13 eqtri 
 |-  W = ( Base ` T )
15 3 fucbas 
 |-  ( C Func E ) = ( Base ` Q )
16 eqid 
 |-  ( C Nat E ) = ( C Nat E )
17 3 16 fuchom 
 |-  ( C Nat E ) = ( Hom ` Q )
18 eqid 
 |-  ( D FuncCat E ) = ( D FuncCat E )
19 18 11 12 fuccat 
 |-  ( ph -> ( D FuncCat E ) e. Cat )
20 eqid 
 |-  ( C FuncCat D ) = ( C FuncCat D )
21 20 10 11 fuccat 
 |-  ( ph -> ( C FuncCat D ) e. Cat )
22 2 19 21 xpccat 
 |-  ( ph -> T e. Cat )
23 3 10 12 fuccat 
 |-  ( ph -> Q e. Cat )
24 14 15 5 17 6 7 8 9 22 23 isfunc 
 |-  ( 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 ) ) ) ) ) )
25 rescofuf 
 |-  ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E )
26 1 reseq2i 
 |-  ( o.func |` W ) = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) )
27 4 26 eqtri 
 |-  O = ( o.func |` ( ( D Func E ) X. ( C Func D ) ) )
28 27 1 feq12i 
 |-  ( O : W --> ( C Func E ) <-> ( o.func |` ( ( D Func E ) X. ( C Func D ) ) ) : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E ) )
29 25 28 mpbir 
 |-  O : W --> ( C Func E )
30 3anass 
 |-  ( ( 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 ) ) ) ) ) )
31 29 30 mpbiran 
 |-  ( ( 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 ) ) ) ) )
32 24 31 bitrdi 
 |-  ( 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 ) ) ) ) ) )
33 2 fveq2i 
 |-  ( Hom ` T ) = ( Hom ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
34 5 33 eqtri 
 |-  H = ( Hom ` ( ( D FuncCat E ) Xc. ( C FuncCat D ) ) )
35 1 34 fucofulem2 
 |-  ( P e. X_ z e. ( W X. W ) ( ( ( O ` ( 1st ` z ) ) ( C Nat E ) ( O ` ( 2nd ` z ) ) ) ^m ( H ` z ) ) <-> ( 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 ) ) ) ) )
36 35 anbi1i 
 |-  ( ( 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 ) ) ) ) )
37 32 36 bitrdi 
 |-  ( 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 ) ) ) ) ) )