Metamath Proof Explorer

Theorem fucidcobi

Description: Componentwise functor laws for a correctly typed hom-family into a functor category. The source category T and object assignment O are arbitrary: the identity and composition laws are equivalent to their component equations. No functor law is assumed in the hypotheses. Functor composition is an application in fucoisfunc2 . (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses fucidcobi.w 
|- W = ( Base ` T )
fucidcobi.q 
|- Q = ( C FuncCat E )
fucidcobi.b 
|- B = ( Base ` C )
fucidcobi.h 
|- H = ( Hom ` T )
fucidcobi.i 
|- I = ( Id ` T )
fucidcobi.j 
|- J = ( Id ` Q )
fucidcobi.k 
|- K = ( Id ` E )
fucidcobi.x 
|- .x. = ( comp ` T )
fucidcobi.y 
|- .o. = ( comp ` Q )
fucidcobi.v 
|- .xb = ( comp ` E )
fucidcobi.c 
|- ( ph -> T e. Cat )
fucidcobi.p 
|- ( ph -> P e. X_ v e. ( W X. W ) ( ( ( O ` ( 1st ` v ) ) ( C Nat E ) ( O ` ( 2nd ` v ) ) ) ^m ( H ` v ) ) )
Assertion fucidcobi 
|- ( ph -> ( 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 ) ) ) <-> 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 fucidcobi.w 
 |-  W = ( Base ` T )
2 fucidcobi.q 
 |-  Q = ( C FuncCat E )
3 fucidcobi.b 
 |-  B = ( Base ` C )
4 fucidcobi.h 
 |-  H = ( Hom ` T )
5 fucidcobi.i 
 |-  I = ( Id ` T )
6 fucidcobi.j 
 |-  J = ( Id ` Q )
7 fucidcobi.k 
 |-  K = ( Id ` E )
8 fucidcobi.x 
 |-  .x. = ( comp ` T )
9 fucidcobi.y 
 |-  .o. = ( comp ` Q )
10 fucidcobi.v 
 |-  .xb = ( comp ` E )
11 fucidcobi.c 
 |-  ( ph -> T e. Cat )
12 fucidcobi.p 
 |-  ( ph -> P e. X_ v e. ( W X. W ) ( ( ( O ` ( 1st ` v ) ) ( C Nat E ) ( O ` ( 2nd ` v ) ) ) ^m ( H ` v ) ) )
13 eqid 
 |-  ( C Nat E ) = ( C Nat E )
14 12 adantr 
 |-  ( ( ph /\ x e. W ) -> P e. X_ v e. ( W X. W ) ( ( ( O ` ( 1st ` v ) ) ( C Nat E ) ( O ` ( 2nd ` v ) ) ) ^m ( H ` v ) ) )
15 simpr 
 |-  ( ( ph /\ x e. W ) -> x e. W )
16 14 15 15 ixpovf 
 |-  ( ( ph /\ x e. W ) -> ( x P x ) : ( x H x ) --> ( ( O ` x ) ( C Nat E ) ( O ` x ) ) )
17 11 adantr 
 |-  ( ( ph /\ x e. W ) -> T e. Cat )
18 1 4 5 17 15 catidcl 
 |-  ( ( ph /\ x e. W ) -> ( I ` x ) e. ( x H x ) )
19 16 18 ffvelcdmd 
 |-  ( ( ph /\ x e. W ) -> ( ( x P x ) ` ( I ` x ) ) e. ( ( O ` x ) ( C Nat E ) ( O ` x ) ) )
20 2 13 3 6 7 19 natideq 
 |-  ( ( ph /\ x e. W ) -> ( ( ( x P x ) ` ( I ` x ) ) = ( J ` ( O ` x ) ) <-> A. t e. B ( ( ( x P x ) ` ( I ` x ) ) ` t ) = ( K ` ( ( 1st ` ( O ` x ) ) ` t ) ) ) )
21 simpl 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) )
22 21 simpld 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) )
23 22 simpld 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( ( ph /\ x e. W ) /\ y e. W ) )
24 23 simpld 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( ph /\ x e. W ) )
25 24 simpld 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ph )
26 25 12 syl 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> P e. X_ v e. ( W X. W ) ( ( ( O ` ( 1st ` v ) ) ( C Nat E ) ( O ` ( 2nd ` v ) ) ) ^m ( H ` v ) ) )
27 24 simprd 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> x e. W )
28 23 simprd 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> y e. W )
29 26 27 28 ixpovf 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( x P y ) : ( x H y ) --> ( ( O ` x ) ( C Nat E ) ( O ` y ) ) )
30 21 simprd 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> m e. ( x H y ) )
31 29 30 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( ( x P y ) ` m ) e. ( ( O ` x ) ( C Nat E ) ( O ` y ) ) )
32 22 simprd 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> z e. W )
33 26 28 32 ixpovf 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( y P z ) : ( y H z ) --> ( ( O ` y ) ( C Nat E ) ( O ` z ) ) )
34 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> n e. ( y H z ) )
35 33 34 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( ( y P z ) ` n ) e. ( ( O ` y ) ( C Nat E ) ( O ` z ) ) )
36 26 27 32 ixpovf 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( x P z ) : ( x H z ) --> ( ( O ` x ) ( C Nat E ) ( O ` z ) ) )
37 25 11 syl 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> T e. Cat )
38 1 4 8 37 27 28 32 30 34 catcocl 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( n ( <. x , y >. .x. z ) m ) e. ( x H z ) )
39 36 38 ffvelcdmd 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ n e. ( y H z ) ) -> ( ( x P z ) ` ( n ( <. x , y >. .x. z ) m ) ) e. ( ( O ` x ) ( C Nat E ) ( O ` z ) ) )
40 2 13 3 10 9 31 35 39 natcoeq 
 |-  ( ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ m e. ( x H y ) ) /\ 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 ) ) <-> 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 ) ) ) )
41 40 ralbidva 
 |-  ( ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ z e. W ) /\ 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 ) ) <-> 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 ) ) ) )
42 41 ralbidva 
 |-  ( ( ( ( ph /\ x e. W ) /\ y e. W ) /\ 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 ) ) <-> 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 ) ) ) )
43 42 ralbidva 
 |-  ( ( ( ph /\ x e. W ) /\ 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 ) ) <-> 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 ) ) ) )
44 43 ralbidva 
 |-  ( ( ph /\ x e. W ) -> ( 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 ) ) <-> 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 ) ) ) )
45 20 44 anbi12d 
 |-  ( ( ph /\ 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 ) ) ) <-> ( 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 ) ) ) ) )
46 45 ralbidva 
 |-  ( ph -> ( 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 ) ) ) <-> 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 ) ) ) ) )