Metamath Proof Explorer

Theorem cidpropd

Description: Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses catpropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
catpropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
catpropd.3 
|- ( ph -> C e. V )
catpropd.4 
|- ( ph -> D e. W )
Assertion cidpropd 
|- ( ph -> ( Id ` C ) = ( Id ` D ) )

Proof

Step Hyp Ref Expression
1 catpropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 catpropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 catpropd.3 
 |-  ( ph -> C e. V )
4 catpropd.4 
 |-  ( ph -> D e. W )
5 1 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
6 5 adantr 
 |-  ( ( ph /\ C e. Cat ) -> ( Base ` C ) = ( Base ` D ) )
7 eqid 
 |-  ( Base ` C ) = ( Base ` C )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
10 1 ad4antr 
 |-  ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) )
11 simpr 
 |-  ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> y e. ( Base ` C ) )
12 simpllr 
 |-  ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> x e. ( Base ` C ) )
13 7 8 9 10 11 12 homfeqval 
 |-  ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( y ( Hom ` C ) x ) = ( y ( Hom ` D ) x ) )
14 eqid 
 |-  ( comp ` C ) = ( comp ` C )
15 eqid 
 |-  ( comp ` D ) = ( comp ` D )
16 1 ad5antr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( Homf ` C ) = ( Homf ` D ) )
17 2 ad5antr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( comf ` C ) = ( comf ` D ) )
18 simplr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> y e. ( Base ` C ) )
19 simp-4r 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> x e. ( Base ` C ) )
20 simpr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> f e. ( y ( Hom ` C ) x ) )
21 simpllr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> g e. ( x ( Hom ` C ) x ) )
22 7 8 14 15 16 17 18 19 19 20 21 comfeqval 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( g ( <. y , x >. ( comp ` C ) x ) f ) = ( g ( <. y , x >. ( comp ` D ) x ) f ) )
23 22 eqeq1d 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( g ( <. y , x >. ( comp ` C ) x ) f ) = f <-> ( g ( <. y , x >. ( comp ` D ) x ) f ) = f ) )
24 13 23 raleqbidva 
 |-  ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f <-> A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f ) )
25 7 8 9 10 12 11 homfeqval 
 |-  ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( x ( Hom ` C ) y ) = ( x ( Hom ` D ) y ) )
26 10 adantr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( Homf ` C ) = ( Homf ` D ) )
27 2 ad5antr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( comf ` C ) = ( comf ` D ) )
28 12 adantr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> x e. ( Base ` C ) )
29 simplr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> y e. ( Base ` C ) )
30 simpllr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> g e. ( x ( Hom ` C ) x ) )
31 simpr 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> f e. ( x ( Hom ` C ) y ) )
32 7 8 14 15 26 27 28 28 29 30 31 comfeqval 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( f ( <. x , x >. ( comp ` C ) y ) g ) = ( f ( <. x , x >. ( comp ` D ) y ) g ) )
33 32 eqeq1d 
 |-  ( ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) /\ f e. ( x ( Hom ` C ) y ) ) -> ( ( f ( <. x , x >. ( comp ` C ) y ) g ) = f <-> ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) )
34 25 33 raleqbidva 
 |-  ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f <-> A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) )
35 24 34 anbi12d 
 |-  ( ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) /\ y e. ( Base ` C ) ) -> ( ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) <-> ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) )
36 35 ralbidva 
 |-  ( ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) /\ g e. ( x ( Hom ` C ) x ) ) -> ( A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) <-> A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) )
37 36 riotabidva 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) -> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) = ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) )
38 1 ad2antrr 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) )
39 simpr 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
40 7 8 9 38 39 39 homfeqval 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) -> ( x ( Hom ` C ) x ) = ( x ( Hom ` D ) x ) )
41 5 ad2antrr 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) -> ( Base ` C ) = ( Base ` D ) )
42 41 raleqdv 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) -> ( A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) <-> A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) )
43 40 42 riotaeqbidv 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) -> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) = ( iota_ g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) )
44 37 43 eqtrd 
 |-  ( ( ( ph /\ C e. Cat ) /\ x e. ( Base ` C ) ) -> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) = ( iota_ g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) )
45 6 44 mpteq12dva 
 |-  ( ( ph /\ C e. Cat ) -> ( x e. ( Base ` C ) |-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) ) = ( x e. ( Base ` D ) |-> ( iota_ g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) ) )
46 simpr 
 |-  ( ( ph /\ C e. Cat ) -> C e. Cat )
47 eqid 
 |-  ( Id ` C ) = ( Id ` C )
48 7 8 14 46 47 cidfval 
 |-  ( ( ph /\ C e. Cat ) -> ( Id ` C ) = ( x e. ( Base ` C ) |-> ( iota_ g e. ( x ( Hom ` C ) x ) A. y e. ( Base ` C ) ( A. f e. ( y ( Hom ` C ) x ) ( g ( <. y , x >. ( comp ` C ) x ) f ) = f /\ A. f e. ( x ( Hom ` C ) y ) ( f ( <. x , x >. ( comp ` C ) y ) g ) = f ) ) ) )
49 eqid 
 |-  ( Base ` D ) = ( Base ` D )
50 1 2 3 4 catpropd 
 |-  ( ph -> ( C e. Cat <-> D e. Cat ) )
51 50 biimpa 
 |-  ( ( ph /\ C e. Cat ) -> D e. Cat )
52 eqid 
 |-  ( Id ` D ) = ( Id ` D )
53 49 9 15 51 52 cidfval 
 |-  ( ( ph /\ C e. Cat ) -> ( Id ` D ) = ( x e. ( Base ` D ) |-> ( iota_ g e. ( x ( Hom ` D ) x ) A. y e. ( Base ` D ) ( A. f e. ( y ( Hom ` D ) x ) ( g ( <. y , x >. ( comp ` D ) x ) f ) = f /\ A. f e. ( x ( Hom ` D ) y ) ( f ( <. x , x >. ( comp ` D ) y ) g ) = f ) ) ) )
54 45 48 53 3eqtr4d 
 |-  ( ( ph /\ C e. Cat ) -> ( Id ` C ) = ( Id ` D ) )
55 simpr 
 |-  ( ( ph /\ -. C e. Cat ) -> -. C e. Cat )
56 cidffn 
 |-  Id Fn Cat
57 56 fndmi 
 |-  dom Id = Cat
58 57 eleq2i 
 |-  ( C e. dom Id <-> C e. Cat )
59 55 58 sylnibr 
 |-  ( ( ph /\ -. C e. Cat ) -> -. C e. dom Id )
60 ndmfv 
 |-  ( -. C e. dom Id -> ( Id ` C ) = (/) )
61 59 60 syl 
 |-  ( ( ph /\ -. C e. Cat ) -> ( Id ` C ) = (/) )
62 57 eleq2i 
 |-  ( D e. dom Id <-> D e. Cat )
63 50 62 bitr4di 
 |-  ( ph -> ( C e. Cat <-> D e. dom Id ) )
64 63 notbid 
 |-  ( ph -> ( -. C e. Cat <-> -. D e. dom Id ) )
65 64 biimpa 
 |-  ( ( ph /\ -. C e. Cat ) -> -. D e. dom Id )
66 ndmfv 
 |-  ( -. D e. dom Id -> ( Id ` D ) = (/) )
67 65 66 syl 
 |-  ( ( ph /\ -. C e. Cat ) -> ( Id ` D ) = (/) )
68 61 67 eqtr4d 
 |-  ( ( ph /\ -. C e. Cat ) -> ( Id ` C ) = ( Id ` D ) )
69 54 68 pm2.61dan 
 |-  ( ph -> ( Id ` C ) = ( Id ` D ) )