Metamath Proof Explorer

Theorem oppccatid

Description: Lemma for oppccat . (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis oppcbas.1 
|- O = ( oppCat ` C )
Assertion oppccatid 
|- ( C e. Cat -> ( O e. Cat /\ ( Id ` O ) = ( Id ` C ) ) )

Proof

Step Hyp Ref Expression
1 oppcbas.1 
 |-  O = ( oppCat ` C )
2 eqid 
 |-  ( Base ` C ) = ( Base ` C )
3 1 2 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
4 3 a1i 
 |-  ( C e. Cat -> ( Base ` C ) = ( Base ` O ) )
5 eqidd 
 |-  ( C e. Cat -> ( Hom ` O ) = ( Hom ` O ) )
6 eqidd 
 |-  ( C e. Cat -> ( comp ` O ) = ( comp ` O ) )
7 1 fvexi 
 |-  O e. _V
8 7 a1i 
 |-  ( C e. Cat -> O e. _V )
9 biid 
 |-  ( ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) <-> ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) )
10 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
11 eqid 
 |-  ( Id ` C ) = ( Id ` C )
12 simpl 
 |-  ( ( C e. Cat /\ y e. ( Base ` C ) ) -> C e. Cat )
13 simpr 
 |-  ( ( C e. Cat /\ y e. ( Base ` C ) ) -> y e. ( Base ` C ) )
14 2 10 11 12 13 catidcl 
 |-  ( ( C e. Cat /\ y e. ( Base ` C ) ) -> ( ( Id ` C ) ` y ) e. ( y ( Hom ` C ) y ) )
15 10 1 oppchom 
 |-  ( y ( Hom ` O ) y ) = ( y ( Hom ` C ) y )
16 14 15 eleqtrrdi 
 |-  ( ( C e. Cat /\ y e. ( Base ` C ) ) -> ( ( Id ` C ) ` y ) e. ( y ( Hom ` O ) y ) )
17 eqid 
 |-  ( comp ` C ) = ( comp ` C )
18 simpr1l 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> x e. ( Base ` C ) )
19 simpr1r 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> y e. ( Base ` C ) )
20 2 17 1 18 19 19 oppcco 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( ( ( Id ` C ) ` y ) ( <. x , y >. ( comp ` O ) y ) f ) = ( f ( <. y , y >. ( comp ` C ) x ) ( ( Id ` C ) ` y ) ) )
21 simpl 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> C e. Cat )
22 simpr31 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> f e. ( x ( Hom ` O ) y ) )
23 10 1 oppchom 
 |-  ( x ( Hom ` O ) y ) = ( y ( Hom ` C ) x )
24 22 23 eleqtrdi 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> f e. ( y ( Hom ` C ) x ) )
25 2 10 11 21 19 17 18 24 catrid 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( f ( <. y , y >. ( comp ` C ) x ) ( ( Id ` C ) ` y ) ) = f )
26 20 25 eqtrd 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( ( ( Id ` C ) ` y ) ( <. x , y >. ( comp ` O ) y ) f ) = f )
27 simpr2l 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> z e. ( Base ` C ) )
28 2 17 1 19 19 27 oppcco 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( g ( <. y , y >. ( comp ` O ) z ) ( ( Id ` C ) ` y ) ) = ( ( ( Id ` C ) ` y ) ( <. z , y >. ( comp ` C ) y ) g ) )
29 simpr32 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> g e. ( y ( Hom ` O ) z ) )
30 10 1 oppchom 
 |-  ( y ( Hom ` O ) z ) = ( z ( Hom ` C ) y )
31 29 30 eleqtrdi 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> g e. ( z ( Hom ` C ) y ) )
32 2 10 11 21 27 17 19 31 catlid 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( ( ( Id ` C ) ` y ) ( <. z , y >. ( comp ` C ) y ) g ) = g )
33 28 32 eqtrd 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( g ( <. y , y >. ( comp ` O ) z ) ( ( Id ` C ) ` y ) ) = g )
34 2 17 1 18 19 27 oppcco 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( g ( <. x , y >. ( comp ` O ) z ) f ) = ( f ( <. z , y >. ( comp ` C ) x ) g ) )
35 2 10 17 21 27 19 18 31 24 catcocl 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( f ( <. z , y >. ( comp ` C ) x ) g ) e. ( z ( Hom ` C ) x ) )
36 34 35 eqeltrd 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( g ( <. x , y >. ( comp ` O ) z ) f ) e. ( z ( Hom ` C ) x ) )
37 10 1 oppchom 
 |-  ( x ( Hom ` O ) z ) = ( z ( Hom ` C ) x )
38 36 37 eleqtrrdi 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( g ( <. x , y >. ( comp ` O ) z ) f ) e. ( x ( Hom ` O ) z ) )
39 simpr2r 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> w e. ( Base ` C ) )
40 simpr33 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> h e. ( z ( Hom ` O ) w ) )
41 10 1 oppchom 
 |-  ( z ( Hom ` O ) w ) = ( w ( Hom ` C ) z )
42 40 41 eleqtrdi 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> h e. ( w ( Hom ` C ) z ) )
43 2 10 17 21 39 27 19 42 31 18 24 catass 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( ( f ( <. z , y >. ( comp ` C ) x ) g ) ( <. w , z >. ( comp ` C ) x ) h ) = ( f ( <. w , y >. ( comp ` C ) x ) ( g ( <. w , z >. ( comp ` C ) y ) h ) ) )
44 2 17 1 18 27 39 oppcco 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( h ( <. x , z >. ( comp ` O ) w ) ( f ( <. z , y >. ( comp ` C ) x ) g ) ) = ( ( f ( <. z , y >. ( comp ` C ) x ) g ) ( <. w , z >. ( comp ` C ) x ) h ) )
45 2 17 1 18 19 39 oppcco 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( ( g ( <. w , z >. ( comp ` C ) y ) h ) ( <. x , y >. ( comp ` O ) w ) f ) = ( f ( <. w , y >. ( comp ` C ) x ) ( g ( <. w , z >. ( comp ` C ) y ) h ) ) )
46 43 44 45 3eqtr4rd 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( ( g ( <. w , z >. ( comp ` C ) y ) h ) ( <. x , y >. ( comp ` O ) w ) f ) = ( h ( <. x , z >. ( comp ` O ) w ) ( f ( <. z , y >. ( comp ` C ) x ) g ) ) )
47 2 17 1 19 27 39 oppcco 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( h ( <. y , z >. ( comp ` O ) w ) g ) = ( g ( <. w , z >. ( comp ` C ) y ) h ) )
48 47 oveq1d 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( ( h ( <. y , z >. ( comp ` O ) w ) g ) ( <. x , y >. ( comp ` O ) w ) f ) = ( ( g ( <. w , z >. ( comp ` C ) y ) h ) ( <. x , y >. ( comp ` O ) w ) f ) )
49 34 oveq2d 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( h ( <. x , z >. ( comp ` O ) w ) ( g ( <. x , y >. ( comp ` O ) z ) f ) ) = ( h ( <. x , z >. ( comp ` O ) w ) ( f ( <. z , y >. ( comp ` C ) x ) g ) ) )
50 46 48 49 3eqtr4d 
 |-  ( ( C e. Cat /\ ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( z e. ( Base ` C ) /\ w e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) /\ h e. ( z ( Hom ` O ) w ) ) ) ) -> ( ( h ( <. y , z >. ( comp ` O ) w ) g ) ( <. x , y >. ( comp ` O ) w ) f ) = ( h ( <. x , z >. ( comp ` O ) w ) ( g ( <. x , y >. ( comp ` O ) z ) f ) ) )
51 4 5 6 8 9 16 26 33 38 50 iscatd2 
 |-  ( C e. Cat -> ( O e. Cat /\ ( Id ` O ) = ( y e. ( Base ` C ) |-> ( ( Id ` C ) ` y ) ) ) )
52 2 11 cidfn 
 |-  ( C e. Cat -> ( Id ` C ) Fn ( Base ` C ) )
53 dffn5 
 |-  ( ( Id ` C ) Fn ( Base ` C ) <-> ( Id ` C ) = ( y e. ( Base ` C ) |-> ( ( Id ` C ) ` y ) ) )
54 52 53 sylib 
 |-  ( C e. Cat -> ( Id ` C ) = ( y e. ( Base ` C ) |-> ( ( Id ` C ) ` y ) ) )
55 54 eqeq2d 
 |-  ( C e. Cat -> ( ( Id ` O ) = ( Id ` C ) <-> ( Id ` O ) = ( y e. ( Base ` C ) |-> ( ( Id ` C ) ` y ) ) ) )
56 55 anbi2d 
 |-  ( C e. Cat -> ( ( O e. Cat /\ ( Id ` O ) = ( Id ` C ) ) <-> ( O e. Cat /\ ( Id ` O ) = ( y e. ( Base ` C ) |-> ( ( Id ` C ) ` y ) ) ) ) )
57 51 56 mpbird 
 |-  ( C e. Cat -> ( O e. Cat /\ ( Id ` O ) = ( Id ` C ) ) )