Metamath Proof Explorer

Theorem imassc

Description: An image of a functor satisfies the subcategory subset relation. (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 )
imassc.j 
|- J = ( Homf ` E )
Assertion imassc 
|- ( ph -> K C_cat J )

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 imassc.j 
 |-  J = ( Homf ` E )
6 eqid 
 |-  ( Base ` D ) = ( Base ` D )
7 eqid 
 |-  ( Base ` E ) = ( Base ` E )
8 6 7 4 funcf1 
 |-  ( ph -> F : ( Base ` D ) --> ( Base ` E ) )
9 8 fimassd 
 |-  ( ph -> ( F " A ) C_ ( Base ` E ) )
10 1 9 eqsstrid 
 |-  ( ph -> S C_ ( Base ` E ) )
11 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
12 4 ad2antrr 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> F ( D Func E ) G )
13 6 7 12 funcf1 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> F : ( Base ` D ) --> ( Base ` E ) )
14 13 ffnd 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> F Fn ( Base ` D ) )
15 simprl 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> m e. ( `' F " { z } ) )
16 fniniseg 
 |-  ( F Fn ( Base ` D ) -> ( m e. ( `' F " { z } ) <-> ( m e. ( Base ` D ) /\ ( F ` m ) = z ) ) )
17 16 biimpa 
 |-  ( ( F Fn ( Base ` D ) /\ m e. ( `' F " { z } ) ) -> ( m e. ( Base ` D ) /\ ( F ` m ) = z ) )
18 14 15 17 syl2anc 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( m e. ( Base ` D ) /\ ( F ` m ) = z ) )
19 18 simpld 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> m e. ( Base ` D ) )
20 simprr 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> n e. ( `' F " { w } ) )
21 fniniseg 
 |-  ( F Fn ( Base ` D ) -> ( n e. ( `' F " { w } ) <-> ( n e. ( Base ` D ) /\ ( F ` n ) = w ) ) )
22 21 biimpa 
 |-  ( ( F Fn ( Base ` D ) /\ n e. ( `' F " { w } ) ) -> ( n e. ( Base ` D ) /\ ( F ` n ) = w ) )
23 14 20 22 syl2anc 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( n e. ( Base ` D ) /\ ( F ` n ) = w ) )
24 23 simpld 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> n e. ( Base ` D ) )
25 6 2 11 12 19 24 funcf2 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( m G n ) : ( m H n ) --> ( ( F ` m ) ( Hom ` E ) ( F ` n ) ) )
26 25 fimassd 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( ( m G n ) " ( m H n ) ) C_ ( ( F ` m ) ( Hom ` E ) ( F ` n ) ) )
27 18 simprd 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( F ` m ) = z )
28 23 simprd 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( F ` n ) = w )
29 27 28 oveq12d 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( ( F ` m ) ( Hom ` E ) ( F ` n ) ) = ( z ( Hom ` E ) w ) )
30 26 29 sseqtrd 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( ( m G n ) " ( m H n ) ) C_ ( z ( Hom ` E ) w ) )
31 30 ralrimivva 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> A. m e. ( `' F " { z } ) A. n e. ( `' F " { w } ) ( ( m G n ) " ( m H n ) ) C_ ( z ( Hom ` E ) w ) )
32 iunss 
 |-  ( U_ p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) C_ ( z ( Hom ` E ) w ) <-> A. p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) C_ ( z ( Hom ` E ) w ) )
33 fveq2 
 |-  ( p = <. m , n >. -> ( G ` p ) = ( G ` <. m , n >. ) )
34 df-ov 
 |-  ( m G n ) = ( G ` <. m , n >. )
35 33 34 eqtr4di 
 |-  ( p = <. m , n >. -> ( G ` p ) = ( m G n ) )
36 fveq2 
 |-  ( p = <. m , n >. -> ( H ` p ) = ( H ` <. m , n >. ) )
37 df-ov 
 |-  ( m H n ) = ( H ` <. m , n >. )
38 36 37 eqtr4di 
 |-  ( p = <. m , n >. -> ( H ` p ) = ( m H n ) )
39 35 38 imaeq12d 
 |-  ( p = <. m , n >. -> ( ( G ` p ) " ( H ` p ) ) = ( ( m G n ) " ( m H n ) ) )
40 39 sseq1d 
 |-  ( p = <. m , n >. -> ( ( ( G ` p ) " ( H ` p ) ) C_ ( z ( Hom ` E ) w ) <-> ( ( m G n ) " ( m H n ) ) C_ ( z ( Hom ` E ) w ) ) )
41 40 ralxp 
 |-  ( A. p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) C_ ( z ( Hom ` E ) w ) <-> A. m e. ( `' F " { z } ) A. n e. ( `' F " { w } ) ( ( m G n ) " ( m H n ) ) C_ ( z ( Hom ` E ) w ) )
42 32 41 bitri 
 |-  ( U_ p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) C_ ( z ( Hom ` E ) w ) <-> A. m e. ( `' F " { z } ) A. n e. ( `' F " { w } ) ( ( m G n ) " ( m H n ) ) C_ ( z ( Hom ` E ) w ) )
43 31 42 sylibr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> U_ p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) C_ ( z ( Hom ` E ) w ) )
44 relfunc 
 |-  Rel ( D Func E )
45 44 brrelex1i 
 |-  ( F ( D Func E ) G -> F e. _V )
46 4 45 syl 
 |-  ( ph -> F e. _V )
47 46 adantr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> F e. _V )
48 simprl 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> z e. S )
49 simprr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> w e. S )
50 47 47 48 49 3 imasubclem3 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z K w ) = U_ p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) )
51 10 adantr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> S C_ ( Base ` E ) )
52 51 48 sseldd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> z e. ( Base ` E ) )
53 51 49 sseldd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> w e. ( Base ` E ) )
54 5 7 11 52 53 homfval 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z J w ) = ( z ( Hom ` E ) w ) )
55 43 50 54 3sstr4d 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z K w ) C_ ( z J w ) )
56 55 ralrimivva 
 |-  ( ph -> A. z e. S A. w e. S ( z K w ) C_ ( z J w ) )
57 46 46 3 imasubclem2 
 |-  ( ph -> K Fn ( S X. S ) )
58 5 7 homffn 
 |-  J Fn ( ( Base ` E ) X. ( Base ` E ) )
59 58 a1i 
 |-  ( ph -> J Fn ( ( Base ` E ) X. ( Base ` E ) ) )
60 fvexd 
 |-  ( ph -> ( Base ` E ) e. _V )
61 57 59 60 isssc 
 |-  ( ph -> ( K C_cat J <-> ( S C_ ( Base ` E ) /\ A. z e. S A. w e. S ( z K w ) C_ ( z J w ) ) ) )
62 10 56 61 mpbir2and 
 |-  ( ph -> K C_cat J )