Metamath Proof Explorer

Theorem imasubc

Description: An image of a full functor is a full subcategory. Remark 4.2(3) of Adamek p. 48. (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 ) ) )
imasubc.f 
|- ( ph -> F ( D Full E ) G )
imasubc.c 
|- C = ( Base ` E )
imasubc.j 
|- J = ( Homf ` E )
Assertion imasubc 
|- ( ph -> ( K Fn ( S X. S ) /\ S C_ C /\ ( J |` ( S X. S ) ) = K ) )

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 imasubc.f 
 |-  ( ph -> F ( D Full E ) G )
5 imasubc.c 
 |-  C = ( Base ` E )
6 imasubc.j 
 |-  J = ( Homf ` E )
7 relfull 
 |-  Rel ( D Full E )
8 7 brrelex1i 
 |-  ( F ( D Full E ) G -> F e. _V )
9 4 8 syl 
 |-  ( ph -> F e. _V )
10 9 9 3 imasubclem2 
 |-  ( ph -> K Fn ( S X. S ) )
11 eqid 
 |-  ( Base ` D ) = ( Base ` D )
12 fullfunc 
 |-  ( D Full E ) C_ ( D Func E )
13 12 ssbri 
 |-  ( F ( D Full E ) G -> F ( D Func E ) G )
14 4 13 syl 
 |-  ( ph -> F ( D Func E ) G )
15 11 5 14 funcf1 
 |-  ( ph -> F : ( Base ` D ) --> C )
16 15 fimassd 
 |-  ( ph -> ( F " A ) C_ C )
17 1 16 eqsstrid 
 |-  ( ph -> S C_ C )
18 simprl 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> z e. S )
19 18 1 eleqtrdi 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> z e. ( F " A ) )
20 inisegn0a 
 |-  ( z e. ( F " A ) -> ( `' F " { z } ) =/= (/) )
21 19 20 syl 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( `' F " { z } ) =/= (/) )
22 simprr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> w e. S )
23 22 1 eleqtrdi 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> w e. ( F " A ) )
24 inisegn0a 
 |-  ( w e. ( F " A ) -> ( `' F " { w } ) =/= (/) )
25 23 24 syl 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( `' F " { w } ) =/= (/) )
26 21 25 jca 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( `' F " { z } ) =/= (/) /\ ( `' F " { w } ) =/= (/) ) )
27 xpnz 
 |-  ( ( ( `' F " { z } ) =/= (/) /\ ( `' F " { w } ) =/= (/) ) <-> ( ( `' F " { z } ) X. ( `' F " { w } ) ) =/= (/) )
28 26 27 sylib 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( ( `' F " { z } ) X. ( `' F " { w } ) ) =/= (/) )
29 15 ffnd 
 |-  ( ph -> F Fn ( Base ` D ) )
30 29 ad2antrr 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> F Fn ( Base ` D ) )
31 simprl 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> m e. ( `' F " { z } ) )
32 fniniseg 
 |-  ( F Fn ( Base ` D ) -> ( m e. ( `' F " { z } ) <-> ( m e. ( Base ` D ) /\ ( F ` m ) = z ) ) )
33 32 biimpa 
 |-  ( ( F Fn ( Base ` D ) /\ m e. ( `' F " { z } ) ) -> ( m e. ( Base ` D ) /\ ( F ` m ) = z ) )
34 30 31 33 syl2anc 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( m e. ( Base ` D ) /\ ( F ` m ) = z ) )
35 34 simprd 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( F ` m ) = z )
36 simprr 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> n e. ( `' F " { w } ) )
37 fniniseg 
 |-  ( F Fn ( Base ` D ) -> ( n e. ( `' F " { w } ) <-> ( n e. ( Base ` D ) /\ ( F ` n ) = w ) ) )
38 37 biimpa 
 |-  ( ( F Fn ( Base ` D ) /\ n e. ( `' F " { w } ) ) -> ( n e. ( Base ` D ) /\ ( F ` n ) = w ) )
39 30 36 38 syl2anc 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( n e. ( Base ` D ) /\ ( F ` n ) = w ) )
40 39 simprd 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( F ` n ) = w )
41 35 40 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 ) )
42 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
43 4 ad2antrr 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> F ( D Full E ) G )
44 34 simpld 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> m e. ( Base ` D ) )
45 39 simpld 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> n e. ( Base ` D ) )
46 11 42 2 43 44 45 fullfo 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( m G n ) : ( m H n ) -onto-> ( ( F ` m ) ( Hom ` E ) ( F ` n ) ) )
47 foeq3 
 |-  ( ( ( F ` m ) ( Hom ` E ) ( F ` n ) ) = ( z ( Hom ` E ) w ) -> ( ( m G n ) : ( m H n ) -onto-> ( ( F ` m ) ( Hom ` E ) ( F ` n ) ) <-> ( m G n ) : ( m H n ) -onto-> ( z ( Hom ` E ) w ) ) )
48 47 biimpa 
 |-  ( ( ( ( F ` m ) ( Hom ` E ) ( F ` n ) ) = ( z ( Hom ` E ) w ) /\ ( m G n ) : ( m H n ) -onto-> ( ( F ` m ) ( Hom ` E ) ( F ` n ) ) ) -> ( m G n ) : ( m H n ) -onto-> ( z ( Hom ` E ) w ) )
49 41 46 48 syl2anc 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( m G n ) : ( m H n ) -onto-> ( z ( Hom ` E ) w ) )
50 foima 
 |-  ( ( m G n ) : ( m H n ) -onto-> ( z ( Hom ` E ) w ) -> ( ( m G n ) " ( m H n ) ) = ( z ( Hom ` E ) w ) )
51 49 50 syl 
 |-  ( ( ( ph /\ ( z e. S /\ w e. S ) ) /\ ( m e. ( `' F " { z } ) /\ n e. ( `' F " { w } ) ) ) -> ( ( m G n ) " ( m H n ) ) = ( z ( Hom ` E ) w ) )
52 51 ralrimivva 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> A. m e. ( `' F " { z } ) A. n e. ( `' F " { w } ) ( ( m G n ) " ( m H n ) ) = ( z ( Hom ` E ) w ) )
53 fveq2 
 |-  ( p = <. m , n >. -> ( G ` p ) = ( G ` <. m , n >. ) )
54 df-ov 
 |-  ( m G n ) = ( G ` <. m , n >. )
55 53 54 eqtr4di 
 |-  ( p = <. m , n >. -> ( G ` p ) = ( m G n ) )
56 fveq2 
 |-  ( p = <. m , n >. -> ( H ` p ) = ( H ` <. m , n >. ) )
57 df-ov 
 |-  ( m H n ) = ( H ` <. m , n >. )
58 56 57 eqtr4di 
 |-  ( p = <. m , n >. -> ( H ` p ) = ( m H n ) )
59 55 58 imaeq12d 
 |-  ( p = <. m , n >. -> ( ( G ` p ) " ( H ` p ) ) = ( ( m G n ) " ( m H n ) ) )
60 59 eqeq1d 
 |-  ( p = <. m , n >. -> ( ( ( G ` p ) " ( H ` p ) ) = ( z ( Hom ` E ) w ) <-> ( ( m G n ) " ( m H n ) ) = ( z ( Hom ` E ) w ) ) )
61 60 ralxp 
 |-  ( A. p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) = ( z ( Hom ` E ) w ) <-> A. m e. ( `' F " { z } ) A. n e. ( `' F " { w } ) ( ( m G n ) " ( m H n ) ) = ( z ( Hom ` E ) w ) )
62 52 61 sylibr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> A. p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) = ( z ( Hom ` E ) w ) )
63 iuneqconst2 
 |-  ( ( ( ( `' F " { z } ) X. ( `' F " { w } ) ) =/= (/) /\ A. p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) = ( z ( Hom ` E ) w ) ) -> U_ p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) = ( z ( Hom ` E ) w ) )
64 28 62 63 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> U_ p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) = ( z ( Hom ` E ) w ) )
65 9 adantr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> F e. _V )
66 65 65 18 22 3 imasubclem3 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z K w ) = U_ p e. ( ( `' F " { z } ) X. ( `' F " { w } ) ) ( ( G ` p ) " ( H ` p ) ) )
67 17 adantr 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> S C_ C )
68 67 18 sseldd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> z e. C )
69 67 22 sseldd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> w e. C )
70 6 5 42 68 69 homfval 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z J w ) = ( z ( Hom ` E ) w ) )
71 64 66 70 3eqtr4rd 
 |-  ( ( ph /\ ( z e. S /\ w e. S ) ) -> ( z J w ) = ( z K w ) )
72 71 ralrimivva 
 |-  ( ph -> A. z e. S A. w e. S ( z J w ) = ( z K w ) )
73 fveq2 
 |-  ( q = <. z , w >. -> ( J ` q ) = ( J ` <. z , w >. ) )
74 df-ov 
 |-  ( z J w ) = ( J ` <. z , w >. )
75 73 74 eqtr4di 
 |-  ( q = <. z , w >. -> ( J ` q ) = ( z J w ) )
76 fveq2 
 |-  ( q = <. z , w >. -> ( K ` q ) = ( K ` <. z , w >. ) )
77 df-ov 
 |-  ( z K w ) = ( K ` <. z , w >. )
78 76 77 eqtr4di 
 |-  ( q = <. z , w >. -> ( K ` q ) = ( z K w ) )
79 75 78 eqeq12d 
 |-  ( q = <. z , w >. -> ( ( J ` q ) = ( K ` q ) <-> ( z J w ) = ( z K w ) ) )
80 79 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 ) )
81 72 80 sylibr 
 |-  ( ph -> A. q e. ( S X. S ) ( J ` q ) = ( K ` q ) )
82 6 5 homffn 
 |-  J Fn ( C X. C )
83 82 a1i 
 |-  ( ph -> J Fn ( C X. C ) )
84 xpss12 
 |-  ( ( S C_ C /\ S C_ C ) -> ( S X. S ) C_ ( C X. C ) )
85 17 17 84 syl2anc 
 |-  ( ph -> ( S X. S ) C_ ( C X. C ) )
86 fvreseq1 
 |-  ( ( ( J Fn ( C X. C ) /\ K Fn ( S X. S ) ) /\ ( S X. S ) C_ ( C X. C ) ) -> ( ( J |` ( S X. S ) ) = K <-> A. q e. ( S X. S ) ( J ` q ) = ( K ` q ) ) )
87 83 10 85 86 syl21anc 
 |-  ( ph -> ( ( J |` ( S X. S ) ) = K <-> A. q e. ( S X. S ) ( J ` q ) = ( K ` q ) ) )
88 81 87 mpbird 
 |-  ( ph -> ( J |` ( S X. S ) ) = K )
89 10 17 88 3jca 
 |-  ( ph -> ( K Fn ( S X. S ) /\ S C_ C /\ ( J |` ( S X. S ) ) = K ) )