Metamath Proof Explorer

Theorem fullpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same full 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 fullpropd 
|- ( ph -> ( A Full C ) = ( B Full 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 relfull 
 |-  Rel ( A Full C )
10 relfull 
 |-  Rel ( B Full D )
11 1 homfeqbas 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
12 11 adantr 
 |-  ( ( ph /\ f ( A Func C ) g ) -> ( Base ` A ) = ( Base ` B ) )
13 12 adantr 
 |-  ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) -> ( Base ` A ) = ( Base ` B ) )
14 eqid 
 |-  ( Base ` C ) = ( Base ` C )
15 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
16 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
17 3 ad3antrrr 
 |-  ( ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( Homf ` C ) = ( Homf ` D ) )
18 eqid 
 |-  ( Base ` A ) = ( Base ` A )
19 simpllr 
 |-  ( ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> f ( A Func C ) g )
20 18 14 19 funcf1 
 |-  ( ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> f : ( Base ` A ) --> ( Base ` C ) )
21 simplr 
 |-  ( ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> x e. ( Base ` A ) )
22 20 21 ffvelrnd 
 |-  ( ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( f ` x ) e. ( Base ` C ) )
23 simpr 
 |-  ( ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> y e. ( Base ` A ) )
24 20 23 ffvelrnd 
 |-  ( ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( f ` y ) e. ( Base ` C ) )
25 14 15 16 17 22 24 homfeqval 
 |-  ( ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( ( f ` x ) ( Hom ` C ) ( f ` y ) ) = ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) )
26 25 eqeq2d 
 |-  ( ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) /\ y e. ( Base ` A ) ) -> ( ran ( x g y ) = ( ( f ` x ) ( Hom ` C ) ( f ` y ) ) <-> ran ( x g y ) = ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) )
27 13 26 raleqbidva 
 |-  ( ( ( ph /\ f ( A Func C ) g ) /\ x e. ( Base ` A ) ) -> ( A. y e. ( Base ` A ) ran ( x g y ) = ( ( f ` x ) ( Hom ` C ) ( f ` y ) ) <-> A. y e. ( Base ` B ) ran ( x g y ) = ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) )
28 12 27 raleqbidva 
 |-  ( ( ph /\ f ( A Func C ) g ) -> ( A. x e. ( Base ` A ) A. y e. ( Base ` A ) ran ( x g y ) = ( ( f ` x ) ( Hom ` C ) ( f ` y ) ) <-> A. x e. ( Base ` B ) A. y e. ( Base ` B ) ran ( x g y ) = ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) )
29 28 pm5.32da 
 |-  ( ph -> ( ( f ( A Func C ) g /\ A. x e. ( Base ` A ) A. y e. ( Base ` A ) ran ( x g y ) = ( ( f ` x ) ( Hom ` C ) ( f ` y ) ) ) <-> ( f ( A Func C ) g /\ A. x e. ( Base ` B ) A. y e. ( Base ` B ) ran ( x g y ) = ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) ) )
30 1 2 3 4 5 6 7 8 funcpropd 
 |-  ( ph -> ( A Func C ) = ( B Func D ) )
31 30 breqd 
 |-  ( ph -> ( f ( A Func C ) g <-> f ( B Func D ) g ) )
32 31 anbi1d 
 |-  ( ph -> ( ( f ( A Func C ) g /\ A. x e. ( Base ` B ) A. y e. ( Base ` B ) ran ( x g y ) = ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) <-> ( f ( B Func D ) g /\ A. x e. ( Base ` B ) A. y e. ( Base ` B ) ran ( x g y ) = ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) ) )
33 29 32 bitrd 
 |-  ( ph -> ( ( f ( A Func C ) g /\ A. x e. ( Base ` A ) A. y e. ( Base ` A ) ran ( x g y ) = ( ( f ` x ) ( Hom ` C ) ( f ` y ) ) ) <-> ( f ( B Func D ) g /\ A. x e. ( Base ` B ) A. y e. ( Base ` B ) ran ( x g y ) = ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) ) )
34 18 15 isfull 
 |-  ( f ( A Full C ) g <-> ( f ( A Func C ) g /\ A. x e. ( Base ` A ) A. y e. ( Base ` A ) ran ( x g y ) = ( ( f ` x ) ( Hom ` C ) ( f ` y ) ) ) )
35 eqid 
 |-  ( Base ` B ) = ( Base ` B )
36 35 16 isfull 
 |-  ( f ( B Full D ) g <-> ( f ( B Func D ) g /\ A. x e. ( Base ` B ) A. y e. ( Base ` B ) ran ( x g y ) = ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) )
37 33 34 36 3bitr4g 
 |-  ( ph -> ( f ( A Full C ) g <-> f ( B Full D ) g ) )
38 9 10 37 eqbrrdiv 
 |-  ( ph -> ( A Full C ) = ( B Full D ) )