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

Metamath Proof Explorer

Theorem homfeq

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

Ref Expression
Hypotheses homfeq.h 
|- H = ( Hom ` C )
homfeq.j 
|- J = ( Hom ` D )
homfeq.1 
|- ( ph -> B = ( Base ` C ) )
homfeq.2 
|- ( ph -> B = ( Base ` D ) )
Assertion homfeq 
|- ( ph -> ( ( Homf ` C ) = ( Homf ` D ) <-> A. x e. B A. y e. B ( x H y ) = ( x J y ) ) )

Proof

Step Hyp Ref Expression
1 homfeq.h 
 |-  H = ( Hom ` C )
2 homfeq.j 
 |-  J = ( Hom ` D )
3 homfeq.1 
 |-  ( ph -> B = ( Base ` C ) )
4 homfeq.2 
 |-  ( ph -> B = ( Base ` D ) )
5 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 5 6 1 homffval 
 |-  ( Homf ` C ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x H y ) )
8 eqidd 
 |-  ( ph -> ( x H y ) = ( x H y ) )
9 3 3 8 mpoeq123dv 
 |-  ( ph -> ( x e. B , y e. B |-> ( x H y ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( x H y ) ) )
10 7 9 eqtr4id 
 |-  ( ph -> ( Homf ` C ) = ( x e. B , y e. B |-> ( x H y ) ) )
11 eqid 
 |-  ( Homf ` D ) = ( Homf ` D )
12 eqid 
 |-  ( Base ` D ) = ( Base ` D )
13 11 12 2 homffval 
 |-  ( Homf ` D ) = ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x J y ) )
14 eqidd 
 |-  ( ph -> ( x J y ) = ( x J y ) )
15 4 4 14 mpoeq123dv 
 |-  ( ph -> ( x e. B , y e. B |-> ( x J y ) ) = ( x e. ( Base ` D ) , y e. ( Base ` D ) |-> ( x J y ) ) )
16 13 15 eqtr4id 
 |-  ( ph -> ( Homf ` D ) = ( x e. B , y e. B |-> ( x J y ) ) )
17 10 16 eqeq12d 
 |-  ( ph -> ( ( Homf ` C ) = ( Homf ` D ) <-> ( x e. B , y e. B |-> ( x H y ) ) = ( x e. B , y e. B |-> ( x J y ) ) ) )
18 ovex 
 |-  ( x H y ) e. _V
19 18 rgen2w 
 |-  A. x e. B A. y e. B ( x H y ) e. _V
20 mpo2eqb 
 |-  ( A. x e. B A. y e. B ( x H y ) e. _V -> ( ( x e. B , y e. B |-> ( x H y ) ) = ( x e. B , y e. B |-> ( x J y ) ) <-> A. x e. B A. y e. B ( x H y ) = ( x J y ) ) )
21 19 20 ax-mp 
 |-  ( ( x e. B , y e. B |-> ( x H y ) ) = ( x e. B , y e. B |-> ( x J y ) ) <-> A. x e. B A. y e. B ( x H y ) = ( x J y ) )
22 17 21 bitrdi 
 |-  ( ph -> ( ( Homf ` C ) = ( Homf ` D ) <-> A. x e. B A. y e. B ( x H y ) = ( x J y ) ) )