Metamath Proof Explorer

Theorem imaf1co

Description: An image of a functor whose object part is injective preserves the composition. (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 )
imaf1co.b 
|- B = ( Base ` D )
imaf1co.c 
|- C = ( Base ` E )
imaf1co.o 
|- .xb = ( comp ` E )
imaf1co.f 
|- ( ph -> F : B -1-1-> C )
imaf1co.x 
|- ( ph -> X e. S )
imaf1co.y 
|- ( ph -> Y e. S )
imaf1co.z 
|- ( ph -> Z e. S )
imaf1co.m 
|- ( ph -> M e. ( X K Y ) )
imaf1co.n 
|- ( ph -> N e. ( Y K Z ) )
Assertion imaf1co 
|- ( ph -> ( N ( <. X , Y >. .xb Z ) M ) e. ( X K Z ) )

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 imaf1co.b 
 |-  B = ( Base ` D )
6 imaf1co.c 
 |-  C = ( Base ` E )
7 imaf1co.o 
 |-  .xb = ( comp ` E )
8 imaf1co.f 
 |-  ( ph -> F : B -1-1-> C )
9 imaf1co.x 
 |-  ( ph -> X e. S )
10 imaf1co.y 
 |-  ( ph -> Y e. S )
11 imaf1co.z 
 |-  ( ph -> Z e. S )
12 imaf1co.m 
 |-  ( ph -> M e. ( X K Y ) )
13 imaf1co.n 
 |-  ( ph -> N e. ( Y K Z ) )
14 eqid 
 |-  ( comp ` D ) = ( comp ` D )
15 4 funcrcl2 
 |-  ( ph -> D e. Cat )
16 15 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> D e. Cat )
17 1 8 9 imasubc3lem1 
 |-  ( ph -> ( { ( `' F ` X ) } = ( `' F " { X } ) /\ ( F ` ( `' F ` X ) ) = X /\ ( `' F ` X ) e. B ) )
18 17 simp3d 
 |-  ( ph -> ( `' F ` X ) e. B )
19 18 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( `' F ` X ) e. B )
20 1 8 10 imasubc3lem1 
 |-  ( ph -> ( { ( `' F ` Y ) } = ( `' F " { Y } ) /\ ( F ` ( `' F ` Y ) ) = Y /\ ( `' F ` Y ) e. B ) )
21 20 simp3d 
 |-  ( ph -> ( `' F ` Y ) e. B )
22 21 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( `' F ` Y ) e. B )
23 1 8 11 imasubc3lem1 
 |-  ( ph -> ( { ( `' F ` Z ) } = ( `' F " { Z } ) /\ ( F ` ( `' F ` Z ) ) = Z /\ ( `' F ` Z ) e. B ) )
24 23 simp3d 
 |-  ( ph -> ( `' F ` Z ) e. B )
25 24 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( `' F ` Z ) e. B )
26 simp-4r 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> m e. ( ( `' F ` X ) H ( `' F ` Y ) ) )
27 simplr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) )
28 5 2 14 16 19 22 25 26 27 catcocl 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( n ( <. ( `' F ` X ) , ( `' F ` Y ) >. ( comp ` D ) ( `' F ` Z ) ) m ) e. ( ( `' F ` X ) H ( `' F ` Z ) ) )
29 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
30 5 2 29 4 18 24 funcf2 
 |-  ( ph -> ( ( `' F ` X ) G ( `' F ` Z ) ) : ( ( `' F ` X ) H ( `' F ` Z ) ) --> ( ( F ` ( `' F ` X ) ) ( Hom ` E ) ( F ` ( `' F ` Z ) ) ) )
31 30 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( ( `' F ` X ) G ( `' F ` Z ) ) : ( ( `' F ` X ) H ( `' F ` Z ) ) --> ( ( F ` ( `' F ` X ) ) ( Hom ` E ) ( F ` ( `' F ` Z ) ) ) )
32 31 funfvima2d 
 |-  ( ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) /\ ( n ( <. ( `' F ` X ) , ( `' F ` Y ) >. ( comp ` D ) ( `' F ` Z ) ) m ) e. ( ( `' F ` X ) H ( `' F ` Z ) ) ) -> ( ( ( `' F ` X ) G ( `' F ` Z ) ) ` ( n ( <. ( `' F ` X ) , ( `' F ` Y ) >. ( comp ` D ) ( `' F ` Z ) ) m ) ) e. ( ( ( `' F ` X ) G ( `' F ` Z ) ) " ( ( `' F ` X ) H ( `' F ` Z ) ) ) )
33 28 32 mpdan 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( ( ( `' F ` X ) G ( `' F ` Z ) ) ` ( n ( <. ( `' F ` X ) , ( `' F ` Y ) >. ( comp ` D ) ( `' F ` Z ) ) m ) ) e. ( ( ( `' F ` X ) G ( `' F ` Z ) ) " ( ( `' F ` X ) H ( `' F ` Z ) ) ) )
34 4 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> F ( D Func E ) G )
35 5 2 14 7 34 19 22 25 26 27 funcco 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( ( ( `' F ` X ) G ( `' F ` Z ) ) ` ( n ( <. ( `' F ` X ) , ( `' F ` Y ) >. ( comp ` D ) ( `' F ` Z ) ) m ) ) = ( ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) ( <. ( F ` ( `' F ` X ) ) , ( F ` ( `' F ` Y ) ) >. .xb ( F ` ( `' F ` Z ) ) ) ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) ) )
36 17 simp2d 
 |-  ( ph -> ( F ` ( `' F ` X ) ) = X )
37 36 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( F ` ( `' F ` X ) ) = X )
38 20 simp2d 
 |-  ( ph -> ( F ` ( `' F ` Y ) ) = Y )
39 38 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( F ` ( `' F ` Y ) ) = Y )
40 37 39 opeq12d 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> <. ( F ` ( `' F ` X ) ) , ( F ` ( `' F ` Y ) ) >. = <. X , Y >. )
41 23 simp2d 
 |-  ( ph -> ( F ` ( `' F ` Z ) ) = Z )
42 41 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( F ` ( `' F ` Z ) ) = Z )
43 40 42 oveq12d 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( <. ( F ` ( `' F ` X ) ) , ( F ` ( `' F ` Y ) ) >. .xb ( F ` ( `' F ` Z ) ) ) = ( <. X , Y >. .xb Z ) )
44 simpr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N )
45 simpllr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M )
46 43 44 45 oveq123d 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) ( <. ( F ` ( `' F ` X ) ) , ( F ` ( `' F ` Y ) ) >. .xb ( F ` ( `' F ` Z ) ) ) ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) ) = ( N ( <. X , Y >. .xb Z ) M ) )
47 35 46 eqtr2d 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( N ( <. X , Y >. .xb Z ) M ) = ( ( ( `' F ` X ) G ( `' F ` Z ) ) ` ( n ( <. ( `' F ` X ) , ( `' F ` Y ) >. ( comp ` D ) ( `' F ` Z ) ) m ) ) )
48 relfunc 
 |-  Rel ( D Func E )
49 48 brrelex1i 
 |-  ( F ( D Func E ) G -> F e. _V )
50 4 49 syl 
 |-  ( ph -> F e. _V )
51 1 8 9 11 50 3 imasubc3lem2 
 |-  ( ph -> ( X K Z ) = ( ( ( `' F ` X ) G ( `' F ` Z ) ) " ( ( `' F ` X ) H ( `' F ` Z ) ) ) )
52 51 ad4antr 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( X K Z ) = ( ( ( `' F ` X ) G ( `' F ` Z ) ) " ( ( `' F ` X ) H ( `' F ` Z ) ) ) )
53 33 47 52 3eltr4d 
 |-  ( ( ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) /\ n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ) /\ ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N ) -> ( N ( <. X , Y >. .xb Z ) M ) e. ( X K Z ) )
54 5 2 29 4 21 24 funcf2 
 |-  ( ph -> ( ( `' F ` Y ) G ( `' F ` Z ) ) : ( ( `' F ` Y ) H ( `' F ` Z ) ) --> ( ( F ` ( `' F ` Y ) ) ( Hom ` E ) ( F ` ( `' F ` Z ) ) ) )
55 54 ffund 
 |-  ( ph -> Fun ( ( `' F ` Y ) G ( `' F ` Z ) ) )
56 1 8 10 11 50 3 imasubc3lem2 
 |-  ( ph -> ( Y K Z ) = ( ( ( `' F ` Y ) G ( `' F ` Z ) ) " ( ( `' F ` Y ) H ( `' F ` Z ) ) ) )
57 13 56 eleqtrd 
 |-  ( ph -> N e. ( ( ( `' F ` Y ) G ( `' F ` Z ) ) " ( ( `' F ` Y ) H ( `' F ` Z ) ) ) )
58 fvelima 
 |-  ( ( Fun ( ( `' F ` Y ) G ( `' F ` Z ) ) /\ N e. ( ( ( `' F ` Y ) G ( `' F ` Z ) ) " ( ( `' F ` Y ) H ( `' F ` Z ) ) ) ) -> E. n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N )
59 55 57 58 syl2anc 
 |-  ( ph -> E. n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N )
60 59 ad2antrr 
 |-  ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) -> E. n e. ( ( `' F ` Y ) H ( `' F ` Z ) ) ( ( ( `' F ` Y ) G ( `' F ` Z ) ) ` n ) = N )
61 53 60 r19.29a 
 |-  ( ( ( ph /\ m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ) /\ ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M ) -> ( N ( <. X , Y >. .xb Z ) M ) e. ( X K Z ) )
62 5 2 29 4 18 21 funcf2 
 |-  ( ph -> ( ( `' F ` X ) G ( `' F ` Y ) ) : ( ( `' F ` X ) H ( `' F ` Y ) ) --> ( ( F ` ( `' F ` X ) ) ( Hom ` E ) ( F ` ( `' F ` Y ) ) ) )
63 62 ffund 
 |-  ( ph -> Fun ( ( `' F ` X ) G ( `' F ` Y ) ) )
64 1 8 9 10 50 3 imasubc3lem2 
 |-  ( ph -> ( X K Y ) = ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) ) )
65 12 64 eleqtrd 
 |-  ( ph -> M e. ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) ) )
66 fvelima 
 |-  ( ( Fun ( ( `' F ` X ) G ( `' F ` Y ) ) /\ M e. ( ( ( `' F ` X ) G ( `' F ` Y ) ) " ( ( `' F ` X ) H ( `' F ` Y ) ) ) ) -> E. m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M )
67 63 65 66 syl2anc 
 |-  ( ph -> E. m e. ( ( `' F ` X ) H ( `' F ` Y ) ) ( ( ( `' F ` X ) G ( `' F ` Y ) ) ` m ) = M )
68 61 67 r19.29a 
 |-  ( ph -> ( N ( <. X , Y >. .xb Z ) M ) e. ( X K Z ) )