Metamath Proof Explorer

Theorem imaid

Description: An image of a functor preserves the identity morphism. (Contributed by Zhi Wang, 7-Nov-2025)

Ref Expression
Hypotheses imasubc.s 
|- S = ( F " A )
imasubc.h 
|- H = ( Hom ` D )
imasubc.k 
|- K = ( x e. S , y e. S |-> U_ p e. ( ( `' F " { x } ) X. ( `' F " { y } ) ) ( ( G ` p ) " ( H ` p ) ) )
imassc.f 
|- ( ph -> F ( D Func E ) G )
imaid.i 
|- I = ( Id ` E )
imaid.x 
|- ( ph -> X e. S )
Assertion imaid 
|- ( ph -> ( I ` X ) e. ( X K X ) )

Proof

Step Hyp Ref Expression
1 imasubc.s 
 |-  S = ( F " A )
2 imasubc.h 
 |-  H = ( Hom ` D )
3 imasubc.k 
 |-  K = ( x e. S , y e. S |-> U_ p e. ( ( `' F " { x } ) X. ( `' F " { y } ) ) ( ( G ` p ) " ( H ` p ) ) )
4 imassc.f 
 |-  ( ph -> F ( D Func E ) G )
5 imaid.i 
 |-  I = ( Id ` E )
6 imaid.x 
 |-  ( ph -> X e. S )
7 6 1 eleqtrdi 
 |-  ( ph -> X e. ( F " A ) )
8 inisegn0a 
 |-  ( X e. ( F " A ) -> ( `' F " { X } ) =/= (/) )
9 7 8 syl 
 |-  ( ph -> ( `' F " { X } ) =/= (/) )
10 n0 
 |-  ( ( `' F " { X } ) =/= (/) <-> E. m m e. ( `' F " { X } ) )
11 9 10 sylib 
 |-  ( ph -> E. m m e. ( `' F " { X } ) )
12 fveq2 
 |-  ( p = <. m , m >. -> ( G ` p ) = ( G ` <. m , m >. ) )
13 df-ov 
 |-  ( m G m ) = ( G ` <. m , m >. )
14 12 13 eqtr4di 
 |-  ( p = <. m , m >. -> ( G ` p ) = ( m G m ) )
15 fveq2 
 |-  ( p = <. m , m >. -> ( H ` p ) = ( H ` <. m , m >. ) )
16 df-ov 
 |-  ( m H m ) = ( H ` <. m , m >. )
17 15 16 eqtr4di 
 |-  ( p = <. m , m >. -> ( H ` p ) = ( m H m ) )
18 14 17 imaeq12d 
 |-  ( p = <. m , m >. -> ( ( G ` p ) " ( H ` p ) ) = ( ( m G m ) " ( m H m ) ) )
19 18 eleq2d 
 |-  ( p = <. m , m >. -> ( ( I ` X ) e. ( ( G ` p ) " ( H ` p ) ) <-> ( I ` X ) e. ( ( m G m ) " ( m H m ) ) ) )
20 simpr 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> m e. ( `' F " { X } ) )
21 20 20 opelxpd 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> <. m , m >. e. ( ( `' F " { X } ) X. ( `' F " { X } ) ) )
22 eqid 
 |-  ( Base ` D ) = ( Base ` D )
23 eqid 
 |-  ( Id ` D ) = ( Id ` D )
24 4 adantr 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> F ( D Func E ) G )
25 eqid 
 |-  ( Base ` E ) = ( Base ` E )
26 22 25 4 funcf1 
 |-  ( ph -> F : ( Base ` D ) --> ( Base ` E ) )
27 26 ffnd 
 |-  ( ph -> F Fn ( Base ` D ) )
28 fniniseg 
 |-  ( F Fn ( Base ` D ) -> ( m e. ( `' F " { X } ) <-> ( m e. ( Base ` D ) /\ ( F ` m ) = X ) ) )
29 27 28 syl 
 |-  ( ph -> ( m e. ( `' F " { X } ) <-> ( m e. ( Base ` D ) /\ ( F ` m ) = X ) ) )
30 29 biimpa 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> ( m e. ( Base ` D ) /\ ( F ` m ) = X ) )
31 30 simpld 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> m e. ( Base ` D ) )
32 22 23 5 24 31 funcid 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> ( ( m G m ) ` ( ( Id ` D ) ` m ) ) = ( I ` ( F ` m ) ) )
33 30 simprd 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> ( F ` m ) = X )
34 33 fveq2d 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> ( I ` ( F ` m ) ) = ( I ` X ) )
35 32 34 eqtrd 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> ( ( m G m ) ` ( ( Id ` D ) ` m ) ) = ( I ` X ) )
36 24 funcrcl2 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> D e. Cat )
37 22 2 23 36 31 catidcl 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> ( ( Id ` D ) ` m ) e. ( m H m ) )
38 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
39 22 2 38 24 31 31 funcf2 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> ( m G m ) : ( m H m ) --> ( ( F ` m ) ( Hom ` E ) ( F ` m ) ) )
40 39 funfvima2d 
 |-  ( ( ( ph /\ m e. ( `' F " { X } ) ) /\ ( ( Id ` D ) ` m ) e. ( m H m ) ) -> ( ( m G m ) ` ( ( Id ` D ) ` m ) ) e. ( ( m G m ) " ( m H m ) ) )
41 37 40 mpdan 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> ( ( m G m ) ` ( ( Id ` D ) ` m ) ) e. ( ( m G m ) " ( m H m ) ) )
42 35 41 eqeltrrd 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> ( I ` X ) e. ( ( m G m ) " ( m H m ) ) )
43 19 21 42 rspcedvdw 
 |-  ( ( ph /\ m e. ( `' F " { X } ) ) -> E. p e. ( ( `' F " { X } ) X. ( `' F " { X } ) ) ( I ` X ) e. ( ( G ` p ) " ( H ` p ) ) )
44 11 43 exlimddv 
 |-  ( ph -> E. p e. ( ( `' F " { X } ) X. ( `' F " { X } ) ) ( I ` X ) e. ( ( G ` p ) " ( H ` p ) ) )
45 44 eliund 
 |-  ( ph -> ( I ` X ) e. U_ p e. ( ( `' F " { X } ) X. ( `' F " { X } ) ) ( ( G ` p ) " ( H ` p ) ) )
46 relfunc 
 |-  Rel ( D Func E )
47 46 brrelex1i 
 |-  ( F ( D Func E ) G -> F e. _V )
48 4 47 syl 
 |-  ( ph -> F e. _V )
49 48 48 6 6 3 imasubclem3 
 |-  ( ph -> ( X K X ) = U_ p e. ( ( `' F " { X } ) X. ( `' F " { X } ) ) ( ( G ` p ) " ( H ` p ) ) )
50 45 49 eleqtrrd 
 |-  ( ph -> ( I ` X ) e. ( X K X ) )