Metamath Proof Explorer

Theorem parmapfunc

Description: A map fixing the identity value and preserving the parallel-arrow class induces an endofunctor fixing every object. Category membership and the hom construction suffice: every composable pair contains an identity. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

Ref Expression
Hypotheses parmapfunc.b 
|- B = ( Base ` C )
parmapfunc.h 
|- H = ( Hom ` C )
parmapfunc.c 
|- C e. Cat
parmapfunc.hv 
|- H = ( r e. B , s e. B |-> if ( r = s , { J } , if ( ( r = X /\ s = Y ) , S , (/) ) ) )
parmapfunc.l 
|- L = ( u e. B , v e. B |-> ( a e. ( u H v ) |-> ( A ` a ) ) )
parmapfunc.ai 
|- ( A ` J ) = J
parmapfunc.as 
|- A. t e. S ( A ` t ) e. S
Assertion parmapfunc 
|- ( _I |` B ) ( C Func C ) L

Proof

Step Hyp Ref Expression
1 parmapfunc.b 
 |-  B = ( Base ` C )
2 parmapfunc.h 
 |-  H = ( Hom ` C )
3 parmapfunc.c 
 |-  C e. Cat
4 parmapfunc.hv 
 |-  H = ( r e. B , s e. B |-> if ( r = s , { J } , if ( ( r = X /\ s = Y ) , S , (/) ) ) )
5 parmapfunc.l 
 |-  L = ( u e. B , v e. B |-> ( a e. ( u H v ) |-> ( A ` a ) ) )
6 parmapfunc.ai 
 |-  ( A ` J ) = J
7 parmapfunc.as 
 |-  A. t e. S ( A ` t ) e. S
8 eqid 
 |-  ( Id ` C ) = ( Id ` C )
9 eqid 
 |-  ( comp ` C ) = ( comp ` C )
10 3 a1i 
 |-  ( T. -> C e. Cat )
11 f1oi 
 |-  ( _I |` B ) : B -1-1-onto-> B
12 f1of 
 |-  ( ( _I |` B ) : B -1-1-onto-> B -> ( _I |` B ) : B --> B )
13 11 12 mp1i 
 |-  ( T. -> ( _I |` B ) : B --> B )
14 5 fnmpompt 
 |-  L Fn ( B X. B )
15 14 a1i 
 |-  ( T. -> L Fn ( B X. B ) )
16 simprl 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> x e. B )
17 simprr 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> y e. B )
18 5 16 17 ovmpomptd 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( x L y ) = ( a e. ( x H y ) |-> ( A ` a ) ) )
19 simpr 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B ) ) /\ a e. ( x H y ) ) -> a e. ( x H y ) )
20 6 a1i 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B ) ) /\ a e. ( x H y ) ) -> ( A ` J ) = J )
21 fveq2 
 |-  ( t = a -> ( A ` t ) = ( A ` a ) )
22 21 eleq1d 
 |-  ( t = a -> ( ( A ` t ) e. S <-> ( A ` a ) e. S ) )
23 22 7 vtoclri 
 |-  ( a e. S -> ( A ` a ) e. S )
24 23 adantl 
 |-  ( ( ( ( T. /\ ( x e. B /\ y e. B ) ) /\ a e. ( x H y ) ) /\ a e. S ) -> ( A ` a ) e. S )
25 4 19 20 24 parmapcl 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B ) ) /\ a e. ( x H y ) ) -> ( A ` a ) e. ( x H y ) )
26 18 25 fmpt3d 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( x L y ) : ( x H y ) --> ( x H y ) )
27 fvresi 
 |-  ( x e. B -> ( ( _I |` B ) ` x ) = x )
28 16 27 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( ( _I |` B ) ` x ) = x )
29 fvresi 
 |-  ( y e. B -> ( ( _I |` B ) ` y ) = y )
30 17 29 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( ( _I |` B ) ` y ) = y )
31 28 30 oveq12d 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( ( ( _I |` B ) ` x ) H ( ( _I |` B ) ` y ) ) = ( x H y ) )
32 31 feq3d 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( ( x L y ) : ( x H y ) --> ( ( ( _I |` B ) ` x ) H ( ( _I |` B ) ` y ) ) <-> ( x L y ) : ( x H y ) --> ( x H y ) ) )
33 26 32 mpbird 
 |-  ( ( T. /\ ( x e. B /\ y e. B ) ) -> ( x L y ) : ( x H y ) --> ( ( ( _I |` B ) ` x ) H ( ( _I |` B ) ` y ) ) )
34 3 a1i 
 |-  ( ( T. /\ x e. B ) -> C e. Cat )
35 simpr 
 |-  ( ( T. /\ x e. B ) -> x e. B )
36 1 2 4 34 35 paridval 
 |-  ( ( T. /\ x e. B ) -> ( ( Id ` C ) ` x ) = J )
37 36 fveq2d 
 |-  ( ( T. /\ x e. B ) -> ( ( x L x ) ` ( ( Id ` C ) ` x ) ) = ( ( x L x ) ` J ) )
38 6 eqcomi 
 |-  J = ( A ` J )
39 38 fvexi 
 |-  J e. _V
40 4 39 35 parhomid 
 |-  ( ( T. /\ x e. B ) -> J e. ( x H x ) )
41 5 35 35 40 fvmpomptd 
 |-  ( ( T. /\ x e. B ) -> ( ( x L x ) ` J ) = ( A ` J ) )
42 37 41 eqtrd 
 |-  ( ( T. /\ x e. B ) -> ( ( x L x ) ` ( ( Id ` C ) ` x ) ) = ( A ` J ) )
43 27 adantl 
 |-  ( ( T. /\ x e. B ) -> ( ( _I |` B ) ` x ) = x )
44 43 fveq2d 
 |-  ( ( T. /\ x e. B ) -> ( ( Id ` C ) ` ( ( _I |` B ) ` x ) ) = ( ( Id ` C ) ` x ) )
45 44 36 eqtrd 
 |-  ( ( T. /\ x e. B ) -> ( ( Id ` C ) ` ( ( _I |` B ) ` x ) ) = J )
46 6 42 45 3eqtr4a 
 |-  ( ( T. /\ x e. B ) -> ( ( x L x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` C ) ` ( ( _I |` B ) ` x ) ) )
47 fvif 
 |-  ( A ` if ( x = y , n , m ) ) = if ( x = y , ( A ` n ) , ( A ` m ) )
48 3 a1i 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> C e. Cat )
49 simp3l 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> m e. ( x H y ) )
50 simp3r 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> n e. ( y H z ) )
51 1 2 4 48 9 49 50 parcoval2 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( n ( <. x , y >. ( comp ` C ) z ) m ) = if ( x = y , n , m ) )
52 51 fveq2d 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( x L z ) ` ( n ( <. x , y >. ( comp ` C ) z ) m ) ) = ( ( x L z ) ` if ( x = y , n , m ) ) )
53 simp21 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> x e. B )
54 simp23 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> z e. B )
55 simp22 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> y e. B )
56 1 2 9 48 53 55 54 49 50 catcocl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( n ( <. x , y >. ( comp ` C ) z ) m ) e. ( x H z ) )
57 51 56 eqeltrrd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> if ( x = y , n , m ) e. ( x H z ) )
58 5 53 54 57 fvmpomptd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( x L z ) ` if ( x = y , n , m ) ) = ( A ` if ( x = y , n , m ) ) )
59 52 58 eqtrd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( x L z ) ` ( n ( <. x , y >. ( comp ` C ) z ) m ) ) = ( A ` if ( x = y , n , m ) ) )
60 53 27 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( _I |` B ) ` x ) = x )
61 55 29 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( _I |` B ) ` y ) = y )
62 60 61 opeq12d 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> <. ( ( _I |` B ) ` x ) , ( ( _I |` B ) ` y ) >. = <. x , y >. )
63 fvresi 
 |-  ( z e. B -> ( ( _I |` B ) ` z ) = z )
64 54 63 syl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( _I |` B ) ` z ) = z )
65 62 64 oveq12d 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( <. ( ( _I |` B ) ` x ) , ( ( _I |` B ) ` y ) >. ( comp ` C ) ( ( _I |` B ) ` z ) ) = ( <. x , y >. ( comp ` C ) z ) )
66 5 55 54 50 fvmpomptd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( y L z ) ` n ) = ( A ` n ) )
67 5 53 55 49 fvmpomptd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( x L y ) ` m ) = ( A ` m ) )
68 65 66 67 oveq123d 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( ( y L z ) ` n ) ( <. ( ( _I |` B ) ` x ) , ( ( _I |` B ) ` y ) >. ( comp ` C ) ( ( _I |` B ) ` z ) ) ( ( x L y ) ` m ) ) = ( ( A ` n ) ( <. x , y >. ( comp ` C ) z ) ( A ` m ) ) )
69 6 a1i 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( A ` J ) = J )
70 fveq2 
 |-  ( t = m -> ( A ` t ) = ( A ` m ) )
71 70 eleq1d 
 |-  ( t = m -> ( ( A ` t ) e. S <-> ( A ` m ) e. S ) )
72 71 7 vtoclri 
 |-  ( m e. S -> ( A ` m ) e. S )
73 72 adantl 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) /\ m e. S ) -> ( A ` m ) e. S )
74 4 49 69 73 parmapcl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( A ` m ) e. ( x H y ) )
75 fveq2 
 |-  ( t = n -> ( A ` t ) = ( A ` n ) )
76 75 eleq1d 
 |-  ( t = n -> ( ( A ` t ) e. S <-> ( A ` n ) e. S ) )
77 76 7 vtoclri 
 |-  ( n e. S -> ( A ` n ) e. S )
78 77 adantl 
 |-  ( ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) /\ n e. S ) -> ( A ` n ) e. S )
79 4 50 69 78 parmapcl 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( A ` n ) e. ( y H z ) )
80 1 2 4 48 9 74 79 parcoval2 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( A ` n ) ( <. x , y >. ( comp ` C ) z ) ( A ` m ) ) = if ( x = y , ( A ` n ) , ( A ` m ) ) )
81 68 80 eqtrd 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( ( y L z ) ` n ) ( <. ( ( _I |` B ) ` x ) , ( ( _I |` B ) ` y ) >. ( comp ` C ) ( ( _I |` B ) ` z ) ) ( ( x L y ) ` m ) ) = if ( x = y , ( A ` n ) , ( A ` m ) ) )
82 47 59 81 3eqtr4a 
 |-  ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) /\ ( m e. ( x H y ) /\ n e. ( y H z ) ) ) -> ( ( x L z ) ` ( n ( <. x , y >. ( comp ` C ) z ) m ) ) = ( ( ( y L z ) ` n ) ( <. ( ( _I |` B ) ` x ) , ( ( _I |` B ) ` y ) >. ( comp ` C ) ( ( _I |` B ) ` z ) ) ( ( x L y ) ` m ) ) )
83 1 1 2 2 8 8 9 9 10 10 13 15 33 46 82 isfuncd 
 |-  ( T. -> ( _I |` B ) ( C Func C ) L )
84 83 mptru 
 |-  ( _I |` B ) ( C Func C ) L