Metamath Proof Explorer

Theorem setccatid

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

Ref Expression
Hypothesis setccat.c 
|- C = ( SetCat ` U )
Assertion setccatid 
|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` x ) ) ) )

Proof

Step Hyp Ref Expression
1 setccat.c 
 |-  C = ( SetCat ` U )
2 id 
 |-  ( U e. V -> U e. V )
3 1 2 setcbas 
 |-  ( U e. V -> U = ( Base ` C ) )
4 eqidd 
 |-  ( U e. V -> ( Hom ` C ) = ( Hom ` C ) )
5 eqidd 
 |-  ( U e. V -> ( comp ` C ) = ( comp ` C ) )
6 1 fvexi 
 |-  C e. _V
7 6 a1i 
 |-  ( U e. V -> C e. _V )
8 biid 
 |-  ( ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) <-> ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) )
9 f1oi 
 |-  ( _I |` x ) : x -1-1-onto-> x
10 f1of 
 |-  ( ( _I |` x ) : x -1-1-onto-> x -> ( _I |` x ) : x --> x )
11 9 10 mp1i 
 |-  ( ( U e. V /\ x e. U ) -> ( _I |` x ) : x --> x )
12 simpl 
 |-  ( ( U e. V /\ x e. U ) -> U e. V )
13 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
14 simpr 
 |-  ( ( U e. V /\ x e. U ) -> x e. U )
15 1 12 13 14 14 elsetchom 
 |-  ( ( U e. V /\ x e. U ) -> ( ( _I |` x ) e. ( x ( Hom ` C ) x ) <-> ( _I |` x ) : x --> x ) )
16 11 15 mpbird 
 |-  ( ( U e. V /\ x e. U ) -> ( _I |` x ) e. ( x ( Hom ` C ) x ) )
17 simpl 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> U e. V )
18 eqid 
 |-  ( comp ` C ) = ( comp ` C )
19 simpr1l 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> w e. U )
20 simpr1r 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> x e. U )
21 simpr31 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> f e. ( w ( Hom ` C ) x ) )
22 1 17 13 19 20 elsetchom 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( f e. ( w ( Hom ` C ) x ) <-> f : w --> x ) )
23 21 22 mpbid 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> f : w --> x )
24 9 10 mp1i 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( _I |` x ) : x --> x )
25 1 17 18 19 20 20 23 24 setcco 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( _I |` x ) ( <. w , x >. ( comp ` C ) x ) f ) = ( ( _I |` x ) o. f ) )
26 fcoi2 
 |-  ( f : w --> x -> ( ( _I |` x ) o. f ) = f )
27 23 26 syl 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( _I |` x ) o. f ) = f )
28 25 27 eqtrd 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( _I |` x ) ( <. w , x >. ( comp ` C ) x ) f ) = f )
29 simpr2l 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> y e. U )
30 simpr32 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> g e. ( x ( Hom ` C ) y ) )
31 1 17 13 20 29 elsetchom 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g e. ( x ( Hom ` C ) y ) <-> g : x --> y ) )
32 30 31 mpbid 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> g : x --> y )
33 1 17 18 20 20 29 24 32 setcco 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. x , x >. ( comp ` C ) y ) ( _I |` x ) ) = ( g o. ( _I |` x ) ) )
34 fcoi1 
 |-  ( g : x --> y -> ( g o. ( _I |` x ) ) = g )
35 32 34 syl 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g o. ( _I |` x ) ) = g )
36 33 35 eqtrd 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. x , x >. ( comp ` C ) y ) ( _I |` x ) ) = g )
37 1 17 18 19 20 29 23 32 setcco 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. w , x >. ( comp ` C ) y ) f ) = ( g o. f ) )
38 fco 
 |-  ( ( g : x --> y /\ f : w --> x ) -> ( g o. f ) : w --> y )
39 32 23 38 syl2anc 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g o. f ) : w --> y )
40 1 17 13 19 29 elsetchom 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( g o. f ) e. ( w ( Hom ` C ) y ) <-> ( g o. f ) : w --> y ) )
41 39 40 mpbird 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g o. f ) e. ( w ( Hom ` C ) y ) )
42 37 41 eqeltrd 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. w , x >. ( comp ` C ) y ) f ) e. ( w ( Hom ` C ) y ) )
43 coass 
 |-  ( ( h o. g ) o. f ) = ( h o. ( g o. f ) )
44 simpr2r 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> z e. U )
45 simpr33 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> h e. ( y ( Hom ` C ) z ) )
46 1 17 13 29 44 elsetchom 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h e. ( y ( Hom ` C ) z ) <-> h : y --> z ) )
47 45 46 mpbid 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> h : y --> z )
48 fco 
 |-  ( ( h : y --> z /\ g : x --> y ) -> ( h o. g ) : x --> z )
49 47 32 48 syl2anc 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h o. g ) : x --> z )
50 1 17 18 19 20 44 23 49 setcco 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h o. g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( ( h o. g ) o. f ) )
51 1 17 18 19 29 44 39 47 setcco 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h ( <. w , y >. ( comp ` C ) z ) ( g o. f ) ) = ( h o. ( g o. f ) ) )
52 43 50 51 3eqtr4a 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h o. g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( h ( <. w , y >. ( comp ` C ) z ) ( g o. f ) ) )
53 1 17 18 20 29 44 32 47 setcco 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h ( <. x , y >. ( comp ` C ) z ) g ) = ( h o. g ) )
54 53 oveq1d 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h ( <. x , y >. ( comp ` C ) z ) g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( ( h o. g ) ( <. w , x >. ( comp ` C ) z ) f ) )
55 37 oveq2d 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h ( <. w , y >. ( comp ` C ) z ) ( g ( <. w , x >. ( comp ` C ) y ) f ) ) = ( h ( <. w , y >. ( comp ` C ) z ) ( g o. f ) ) )
56 52 54 55 3eqtr4d 
 |-  ( ( U e. V /\ ( ( w e. U /\ x e. U ) /\ ( y e. U /\ z e. U ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h ( <. x , y >. ( comp ` C ) z ) g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( h ( <. w , y >. ( comp ` C ) z ) ( g ( <. w , x >. ( comp ` C ) y ) f ) ) )
57 3 4 5 7 8 16 28 36 42 56 iscatd2 
 |-  ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` x ) ) ) )