This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem comfeqd

Description: Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfeqd.1 
|- ( ph -> ( comp ` C ) = ( comp ` D ) )
comfeqd.2 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
Assertion comfeqd 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )

Proof

Step Hyp Ref Expression
1 comfeqd.1 
 |-  ( ph -> ( comp ` C ) = ( comp ` D ) )
2 comfeqd.2 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
3 1 oveqd 
 |-  ( ph -> ( <. x , y >. ( comp ` C ) z ) = ( <. x , y >. ( comp ` D ) z ) )
4 3 oveqd 
 |-  ( ph -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
5 4 ralrimivw 
 |-  ( ph -> A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
6 5 ralrimivw 
 |-  ( ph -> A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
7 6 ralrimivw 
 |-  ( ph -> A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
8 7 ralrimivw 
 |-  ( ph -> A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
9 8 ralrimivw 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) )
10 eqid 
 |-  ( comp ` C ) = ( comp ` C )
11 eqid 
 |-  ( comp ` D ) = ( comp ` D )
12 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
13 eqidd 
 |-  ( ph -> ( Base ` C ) = ( Base ` C ) )
14 2 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
15 10 11 12 13 14 2 comfeq 
 |-  ( ph -> ( ( comf ` C ) = ( comf ` D ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` D ) z ) f ) ) )
16 9 15 mpbird 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )