Metamath Proof Explorer

Theorem imaidfu2

Description: The image of the identity functor. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses imaidfu.i 
|- I = ( idFunc ` C )
imaidfu.d 
|- ( ph -> I e. ( D Func E ) )
imaidfu.h 
|- H = ( Hom ` D )
imaidfu.j 
|- J = ( Homf ` D )
imaidfu.k 
|- K = ( x e. S , y e. S |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) )
imaidfu2.s 
|- ( ph -> S = ( Base ` D ) )
Assertion imaidfu2 
|- ( ph -> J = K )

Proof

Step Hyp Ref Expression
1 imaidfu.i 
 |-  I = ( idFunc ` C )
2 imaidfu.d 
 |-  ( ph -> I e. ( D Func E ) )
3 imaidfu.h 
 |-  H = ( Hom ` D )
4 imaidfu.j 
 |-  J = ( Homf ` D )
5 imaidfu.k 
 |-  K = ( x e. S , y e. S |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) )
6 imaidfu2.s 
 |-  ( ph -> S = ( Base ` D ) )
7 eqid 
 |-  ( x e. ( ( 1st ` I ) " ( Base ` D ) ) , y e. ( ( 1st ` I ) " ( Base ` D ) ) |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) ) = ( x e. ( ( 1st ` I ) " ( Base ` D ) ) , y e. ( ( 1st ` I ) " ( Base ` D ) ) |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) )
8 eqid 
 |-  ( ( 1st ` I ) " ( Base ` D ) ) = ( ( 1st ` I ) " ( Base ` D ) )
9 1 2 3 4 7 8 imaidfu 
 |-  ( ph -> ( J |` ( ( ( 1st ` I ) " ( Base ` D ) ) X. ( ( 1st ` I ) " ( Base ` D ) ) ) ) = ( x e. ( ( 1st ` I ) " ( Base ` D ) ) , y e. ( ( 1st ` I ) " ( Base ` D ) ) |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) ) )
10 eqidd 
 |-  ( ph -> ( Base ` D ) = ( Base ` D ) )
11 1 2 10 idfu1sta 
 |-  ( ph -> ( 1st ` I ) = ( _I |` ( Base ` D ) ) )
12 11 imaeq1d 
 |-  ( ph -> ( ( 1st ` I ) " ( Base ` D ) ) = ( ( _I |` ( Base ` D ) ) " ( Base ` D ) ) )
13 ssid 
 |-  ( Base ` D ) C_ ( Base ` D )
14 resiima 
 |-  ( ( Base ` D ) C_ ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) " ( Base ` D ) ) = ( Base ` D ) )
15 13 14 ax-mp 
 |-  ( ( _I |` ( Base ` D ) ) " ( Base ` D ) ) = ( Base ` D )
16 12 15 eqtrdi 
 |-  ( ph -> ( ( 1st ` I ) " ( Base ` D ) ) = ( Base ` D ) )
17 16 sqxpeqd 
 |-  ( ph -> ( ( ( 1st ` I ) " ( Base ` D ) ) X. ( ( 1st ` I ) " ( Base ` D ) ) ) = ( ( Base ` D ) X. ( Base ` D ) ) )
18 17 reseq2d 
 |-  ( ph -> ( J |` ( ( ( 1st ` I ) " ( Base ` D ) ) X. ( ( 1st ` I ) " ( Base ` D ) ) ) ) = ( J |` ( ( Base ` D ) X. ( Base ` D ) ) ) )
19 eqid 
 |-  ( Base ` D ) = ( Base ` D )
20 4 19 homffn 
 |-  J Fn ( ( Base ` D ) X. ( Base ` D ) )
21 fnresdm 
 |-  ( J Fn ( ( Base ` D ) X. ( Base ` D ) ) -> ( J |` ( ( Base ` D ) X. ( Base ` D ) ) ) = J )
22 20 21 ax-mp 
 |-  ( J |` ( ( Base ` D ) X. ( Base ` D ) ) ) = J
23 18 22 eqtrdi 
 |-  ( ph -> ( J |` ( ( ( 1st ` I ) " ( Base ` D ) ) X. ( ( 1st ` I ) " ( Base ` D ) ) ) ) = J )
24 15 12 6 3eqtr4a 
 |-  ( ph -> ( ( 1st ` I ) " ( Base ` D ) ) = S )
25 eqidd 
 |-  ( ph -> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) = U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) )
26 24 24 25 mpoeq123dv 
 |-  ( ph -> ( x e. ( ( 1st ` I ) " ( Base ` D ) ) , y e. ( ( 1st ` I ) " ( Base ` D ) ) |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) ) = ( x e. S , y e. S |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) ) )
27 9 23 26 3eqtr3d 
 |-  ( ph -> J = ( x e. S , y e. S |-> U_ p e. ( ( `' ( 1st ` I ) " { x } ) X. ( `' ( 1st ` I ) " { y } ) ) ( ( ( 2nd ` I ) ` p ) " ( H ` p ) ) ) )
28 27 5 eqtr4di 
 |-  ( ph -> J = K )