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

Metamath Proof Explorer

Theorem fthpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same faithful functors. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fullpropd.1 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
fullpropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
fullpropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
fullpropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
fullpropd.a 
|- ( ph -> A e. V )
fullpropd.b 
|- ( ph -> B e. V )
fullpropd.c 
|- ( ph -> C e. V )
fullpropd.d 
|- ( ph -> D e. V )
Assertion fthpropd 
|- ( ph -> ( A Faith C ) = ( B Faith D ) )

Proof

Step Hyp Ref Expression
1 fullpropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 fullpropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 fullpropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 fullpropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 fullpropd.a 
 |-  ( ph -> A e. V )
6 fullpropd.b 
 |-  ( ph -> B e. V )
7 fullpropd.c 
 |-  ( ph -> C e. V )
8 fullpropd.d 
 |-  ( ph -> D e. V )
9 relfth 
 |-  Rel ( A Faith C )
10 relfth 
 |-  Rel ( B Faith D )
11 1 2 3 4 5 6 7 8 funcpropd 
 |-  ( ph -> ( A Func C ) = ( B Func D ) )
12 11 breqd 
 |-  ( ph -> ( f ( A Func C ) g <-> f ( B Func D ) g ) )
13 1 homfeqbas 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
14 13 raleqdv 
 |-  ( ph -> ( A. y e. ( Base ` A ) Fun `' ( x g y ) <-> A. y e. ( Base ` B ) Fun `' ( x g y ) ) )
15 13 14 raleqbidv 
 |-  ( ph -> ( A. x e. ( Base ` A ) A. y e. ( Base ` A ) Fun `' ( x g y ) <-> A. x e. ( Base ` B ) A. y e. ( Base ` B ) Fun `' ( x g y ) ) )
16 12 15 anbi12d 
 |-  ( ph -> ( ( f ( A Func C ) g /\ A. x e. ( Base ` A ) A. y e. ( Base ` A ) Fun `' ( x g y ) ) <-> ( f ( B Func D ) g /\ A. x e. ( Base ` B ) A. y e. ( Base ` B ) Fun `' ( x g y ) ) ) )
17 eqid 
 |-  ( Base ` A ) = ( Base ` A )
18 17 isfth 
 |-  ( f ( A Faith C ) g <-> ( f ( A Func C ) g /\ A. x e. ( Base ` A ) A. y e. ( Base ` A ) Fun `' ( x g y ) ) )
19 eqid 
 |-  ( Base ` B ) = ( Base ` B )
20 19 isfth 
 |-  ( f ( B Faith D ) g <-> ( f ( B Func D ) g /\ A. x e. ( Base ` B ) A. y e. ( Base ` B ) Fun `' ( x g y ) ) )
21 16 18 20 3bitr4g 
 |-  ( ph -> ( f ( A Faith C ) g <-> f ( B Faith D ) g ) )
22 9 10 21 eqbrrdiv 
 |-  ( ph -> ( A Faith C ) = ( B Faith D ) )