Metamath Proof Explorer

Theorem imaidfu

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 ) ) )
imaidfu.s 
|- S = ( ( 1st ` I ) " A )
Assertion imaidfu 
|- ( ph -> ( J |` ( S X. S ) ) = 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 imaidfu.s 
 |-  S = ( ( 1st ` I ) " A )
7 eqidd 
 |-  ( ph -> ( Base ` D ) = ( Base ` D ) )
8 1 2 7 idfu1sta 
 |-  ( ph -> ( 1st ` I ) = ( _I |` ( Base ` D ) ) )
9 8 adantr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( 1st ` I ) = ( _I |` ( Base ` D ) ) )
10 9 cnveqd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> `' ( 1st ` I ) = `' ( _I |` ( Base ` D ) ) )
11 cnvresid 
 |-  `' ( _I |` ( Base ` D ) ) = ( _I |` ( Base ` D ) )
12 10 11 eqtrdi 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> `' ( 1st ` I ) = ( _I |` ( Base ` D ) ) )
13 12 fveq1d 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( `' ( 1st ` I ) ` z ) = ( ( _I |` ( Base ` D ) ) ` z ) )
14 imassrn 
 |-  ( ( 1st ` I ) " A ) C_ ran ( 1st ` I )
15 6 14 eqsstri 
 |-  S C_ ran ( 1st ` I )
16 8 rneqd 
 |-  ( ph -> ran ( 1st ` I ) = ran ( _I |` ( Base ` D ) ) )
17 rnresi 
 |-  ran ( _I |` ( Base ` D ) ) = ( Base ` D )
18 16 17 eqtrdi 
 |-  ( ph -> ran ( 1st ` I ) = ( Base ` D ) )
19 15 18 sseqtrid 
 |-  ( ph -> S C_ ( Base ` D ) )
20 19 adantr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> S C_ ( Base ` D ) )
21 simprl 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> z e. S )
22 20 21 sseldd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> z e. ( Base ` D ) )
23 fvresi 
 |-  ( z e. ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) ` z ) = z )
24 22 23 syl 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( _I |` ( Base ` D ) ) ` z ) = z )
25 13 24 eqtrd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( `' ( 1st ` I ) ` z ) = z )
26 12 fveq1d 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( `' ( 1st ` I ) ` w ) = ( ( _I |` ( Base ` D ) ) ` w ) )
27 simprr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> w e. S )
28 20 27 sseldd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> w e. ( Base ` D ) )
29 fvresi 
 |-  ( w e. ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) ` w ) = w )
30 28 29 syl 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( _I |` ( Base ` D ) ) ` w ) = w )
31 26 30 eqtrd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( `' ( 1st ` I ) ` w ) = w )
32 25 31 oveq12d 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( `' ( 1st ` I ) ` z ) ( 2nd ` I ) ( `' ( 1st ` I ) ` w ) ) = ( z ( 2nd ` I ) w ) )
33 25 31 oveq12d 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( `' ( 1st ` I ) ` z ) H ( `' ( 1st ` I ) ` w ) ) = ( z H w ) )
34 32 33 imaeq12d 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( ( `' ( 1st ` I ) ` z ) ( 2nd ` I ) ( `' ( 1st ` I ) ` w ) ) " ( ( `' ( 1st ` I ) ` z ) H ( `' ( 1st ` I ) ` w ) ) ) = ( ( z ( 2nd ` I ) w ) " ( z H w ) ) )
35 f1oi 
 |-  ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` D )
36 9 f1oeq1d 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( 1st ` I ) : ( Base ` D ) -1-1-onto-> ( Base ` D ) <-> ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` D ) ) )
37 35 36 mpbiri 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( 1st ` I ) : ( Base ` D ) -1-1-onto-> ( Base ` D ) )
38 f1of1 
 |-  ( ( 1st ` I ) : ( Base ` D ) -1-1-onto-> ( Base ` D ) -> ( 1st ` I ) : ( Base ` D ) -1-1-> ( Base ` D ) )
39 37 38 syl 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( 1st ` I ) : ( Base ` D ) -1-1-> ( Base ` D ) )
40 fvexd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( 1st ` I ) e. _V )
41 6 39 21 27 40 5 imaf1hom 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z K w ) = ( ( ( `' ( 1st ` I ) ` z ) ( 2nd ` I ) ( `' ( 1st ` I ) ` w ) ) " ( ( `' ( 1st ` I ) ` z ) H ( `' ( 1st ` I ) ` w ) ) ) )
42 eqid 
 |-  ( Base ` D ) = ( Base ` D )
43 4 42 3 22 28 homfval 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z J w ) = ( z H w ) )
44 2 adantr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> I e. ( D Func E ) )
45 eqidd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( Base ` D ) = ( Base ` D ) )
46 3 oveqi 
 |-  ( z H w ) = ( z ( Hom ` D ) w )
47 46 a1i 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z H w ) = ( z ( Hom ` D ) w ) )
48 1 44 45 22 28 47 idfu2nda 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z ( 2nd ` I ) w ) = ( _I |` ( z H w ) ) )
49 48 imaeq1d 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( z ( 2nd ` I ) w ) " ( z H w ) ) = ( ( _I |` ( z H w ) ) " ( z H w ) ) )
50 ssid 
 |-  ( z H w ) C_ ( z H w )
51 resiima 
 |-  ( ( z H w ) C_ ( z H w ) -> ( ( _I |` ( z H w ) ) " ( z H w ) ) = ( z H w ) )
52 50 51 ax-mp 
 |-  ( ( _I |` ( z H w ) ) " ( z H w ) ) = ( z H w )
53 49 52 eqtrdi 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( z ( 2nd ` I ) w ) " ( z H w ) ) = ( z H w ) )
54 43 53 eqtr4d 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z J w ) = ( ( z ( 2nd ` I ) w ) " ( z H w ) ) )
55 34 41 54 3eqtr4rd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z J w ) = ( z K w ) )
56 55 ralrimivva 
 |-  ( ph -> A. z e. S A. w e. S ( z J w ) = ( z K w ) )
57 fveq2 
 |-  ( q = <. z , w >. -> ( J ` q ) = ( J ` <. z , w >. ) )
58 df-ov 
 |-  ( z J w ) = ( J ` <. z , w >. )
59 57 58 eqtr4di 
 |-  ( q = <. z , w >. -> ( J ` q ) = ( z J w ) )
60 fveq2 
 |-  ( q = <. z , w >. -> ( K ` q ) = ( K ` <. z , w >. ) )
61 df-ov 
 |-  ( z K w ) = ( K ` <. z , w >. )
62 60 61 eqtr4di 
 |-  ( q = <. z , w >. -> ( K ` q ) = ( z K w ) )
63 59 62 eqeq12d 
 |-  ( q = <. z , w >. -> ( ( J ` q ) = ( K ` q ) <-> ( z J w ) = ( z K w ) ) )
64 63 ralxp 
 |-  ( A. q e. ( S X. S ) ( J ` q ) = ( K ` q ) <-> A. z e. S A. w e. S ( z J w ) = ( z K w ) )
65 56 64 sylibr 
 |-  ( ph -> A. q e. ( S X. S ) ( J ` q ) = ( K ` q ) )
66 4 42 homffn 
 |-  J Fn ( ( Base ` D ) X. ( Base ` D ) )
67 66 a1i 
 |-  ( ph -> J Fn ( ( Base ` D ) X. ( Base ` D ) ) )
68 fvexd 
 |-  ( ph -> ( 1st ` I ) e. _V )
69 68 68 5 imasubclem2 
 |-  ( ph -> K Fn ( S X. S ) )
70 xpss12 
 |-  ( ( S C_ ( Base ` D ) /\ S C_ ( Base ` D ) ) -> ( S X. S ) C_ ( ( Base ` D ) X. ( Base ` D ) ) )
71 19 19 70 syl2anc 
 |-  ( ph -> ( S X. S ) C_ ( ( Base ` D ) X. ( Base ` D ) ) )
72 fvreseq1 
 |-  ( ( ( J Fn ( ( Base ` D ) X. ( Base ` D ) ) /\ K Fn ( S X. S ) ) /\ ( S X. S ) C_ ( ( Base ` D ) X. ( Base ` D ) ) ) -> ( ( J |` ( S X. S ) ) = K <-> A. q e. ( S X. S ) ( J ` q ) = ( K ` q ) ) )
73 67 69 71 72 syl21anc 
 |-  ( ph -> ( ( J |` ( S X. S ) ) = K <-> A. q e. ( S X. S ) ( J ` q ) = ( K ` q ) ) )
74 65 73 mpbird 
 |-  ( ph -> ( J |` ( S X. S ) ) = K )