Metamath Proof Explorer

Theorem fthcomf

Description: Source categories of a faithful functor have the same base, hom-sets and composition operation if the composition is compatible in images of the functor. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses fthcomf.1 
|- ( ph -> F ( A Faith C ) G )
fthcomf.2 
|- ( ph -> F ( B Func D ) G )
fthcomf.3 
|- ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` C ) ( F ` z ) ) ( ( x G y ) ` f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) )
Assertion fthcomf 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )

Proof

Step Hyp Ref Expression
1 fthcomf.1 
 |-  ( ph -> F ( A Faith C ) G )
2 fthcomf.2 
 |-  ( ph -> F ( B Func D ) G )
3 fthcomf.3 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` C ) ( F ` z ) ) ( ( x G y ) ` f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) )
4 eqid 
 |-  ( Base ` A ) = ( Base ` A )
5 eqid 
 |-  ( Hom ` A ) = ( Hom ` A )
6 eqid 
 |-  ( comp ` A ) = ( comp ` A )
7 eqid 
 |-  ( comp ` C ) = ( comp ` C )
8 1 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> F ( A Faith C ) G )
9 fthfunc 
 |-  ( A Faith C ) C_ ( A Func C )
10 9 ssbri 
 |-  ( F ( A Faith C ) G -> F ( A Func C ) G )
11 8 10 syl 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> F ( A Func C ) G )
12 simplr1 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> x e. ( Base ` A ) )
13 simplr2 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> y e. ( Base ` A ) )
14 simplr3 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> z e. ( Base ` A ) )
15 simprl 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> f e. ( x ( Hom ` A ) y ) )
16 simprr 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> g e. ( y ( Hom ` A ) z ) )
17 4 5 6 7 11 12 13 14 15 16 funcco 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( ( x G z ) ` ( g ( <. x , y >. ( comp ` A ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` C ) ( F ` z ) ) ( ( x G y ) ` f ) ) )
18 eqid 
 |-  ( Base ` B ) = ( Base ` B )
19 eqid 
 |-  ( Hom ` B ) = ( Hom ` B )
20 eqid 
 |-  ( comp ` B ) = ( comp ` B )
21 eqid 
 |-  ( comp ` D ) = ( comp ` D )
22 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> F ( B Func D ) G )
23 1 10 syl 
 |-  ( ph -> F ( A Func C ) G )
24 23 2 funchomf 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
25 24 homfeqbas 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
26 25 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( Base ` A ) = ( Base ` B ) )
27 12 26 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> x e. ( Base ` B ) )
28 13 26 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> y e. ( Base ` B ) )
29 14 26 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> z e. ( Base ` B ) )
30 24 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( Homf ` A ) = ( Homf ` B ) )
31 4 5 19 30 12 13 homfeqval 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( x ( Hom ` A ) y ) = ( x ( Hom ` B ) y ) )
32 15 31 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> f e. ( x ( Hom ` B ) y ) )
33 4 5 19 30 13 14 homfeqval 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( y ( Hom ` A ) z ) = ( y ( Hom ` B ) z ) )
34 16 33 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> g e. ( y ( Hom ` B ) z ) )
35 18 19 20 21 22 27 28 29 32 34 funcco 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( ( x G z ) ` ( g ( <. x , y >. ( comp ` B ) z ) f ) ) = ( ( ( y G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( F ` z ) ) ( ( x G y ) ` f ) ) )
36 3 17 35 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( ( x G z ) ` ( g ( <. x , y >. ( comp ` A ) z ) f ) ) = ( ( x G z ) ` ( g ( <. x , y >. ( comp ` B ) z ) f ) ) )
37 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
38 23 funcrcl2 
 |-  ( ph -> A e. Cat )
39 38 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> A e. Cat )
40 4 5 6 39 12 13 14 15 16 catcocl 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( g ( <. x , y >. ( comp ` A ) z ) f ) e. ( x ( Hom ` A ) z ) )
41 2 funcrcl2 
 |-  ( ph -> B e. Cat )
42 41 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> B e. Cat )
43 18 19 20 42 27 28 29 32 34 catcocl 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( g ( <. x , y >. ( comp ` B ) z ) f ) e. ( x ( Hom ` B ) z ) )
44 4 5 19 30 12 14 homfeqval 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( x ( Hom ` A ) z ) = ( x ( Hom ` B ) z ) )
45 43 44 eleqtrrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( g ( <. x , y >. ( comp ` B ) z ) f ) e. ( x ( Hom ` A ) z ) )
46 4 5 37 8 12 14 40 45 fthi 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( ( ( x G z ) ` ( g ( <. x , y >. ( comp ` A ) z ) f ) ) = ( ( x G z ) ` ( g ( <. x , y >. ( comp ` B ) z ) f ) ) <-> ( g ( <. x , y >. ( comp ` A ) z ) f ) = ( g ( <. x , y >. ( comp ` B ) z ) f ) ) )
47 36 46 mpbid 
 |-  ( ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) /\ ( f e. ( x ( Hom ` A ) y ) /\ g e. ( y ( Hom ` A ) z ) ) ) -> ( g ( <. x , y >. ( comp ` A ) z ) f ) = ( g ( <. x , y >. ( comp ` B ) z ) f ) )
48 47 ralrimivva 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) /\ z e. ( Base ` A ) ) ) -> A. f e. ( x ( Hom ` A ) y ) A. g e. ( y ( Hom ` A ) z ) ( g ( <. x , y >. ( comp ` A ) z ) f ) = ( g ( <. x , y >. ( comp ` B ) z ) f ) )
49 48 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. z e. ( Base ` A ) A. f e. ( x ( Hom ` A ) y ) A. g e. ( y ( Hom ` A ) z ) ( g ( <. x , y >. ( comp ` A ) z ) f ) = ( g ( <. x , y >. ( comp ` B ) z ) f ) )
50 eqidd 
 |-  ( ph -> ( Base ` A ) = ( Base ` A ) )
51 6 20 5 50 25 24 comfeq 
 |-  ( ph -> ( ( comf ` A ) = ( comf ` B ) <-> A. x e. ( Base ` A ) A. y e. ( Base ` A ) A. z e. ( Base ` A ) A. f e. ( x ( Hom ` A ) y ) A. g e. ( y ( Hom ` A ) z ) ( g ( <. x , y >. ( comp ` A ) z ) f ) = ( g ( <. x , y >. ( comp ` B ) z ) f ) ) )
52 49 51 mpbird 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )