Metamath Proof Explorer

Theorem catccatid

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

Ref Expression
Hypotheses catccatid.c 
|- C = ( CatCat ` U )
catccatid.b 
|- B = ( Base ` C )
Assertion catccatid 
|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( idFunc ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 catccatid.c 
 |-  C = ( CatCat ` U )
2 catccatid.b 
 |-  B = ( Base ` C )
3 2 a1i 
 |-  ( U e. V -> B = ( 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. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) <-> ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) )
9 id 
 |-  ( U e. V -> U e. V )
10 1 2 9 catcbas 
 |-  ( U e. V -> B = ( U i^i Cat ) )
11 inss2 
 |-  ( U i^i Cat ) C_ Cat
12 10 11 eqsstrdi 
 |-  ( U e. V -> B C_ Cat )
13 12 sselda 
 |-  ( ( U e. V /\ x e. B ) -> x e. Cat )
14 eqid 
 |-  ( idFunc ` x ) = ( idFunc ` x )
15 14 idfucl 
 |-  ( x e. Cat -> ( idFunc ` x ) e. ( x Func x ) )
16 13 15 syl 
 |-  ( ( U e. V /\ x e. B ) -> ( idFunc ` x ) e. ( x Func x ) )
17 simpl 
 |-  ( ( U e. V /\ x e. B ) -> U e. V )
18 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
19 simpr 
 |-  ( ( U e. V /\ x e. B ) -> x e. B )
20 1 2 17 18 19 19 catchom 
 |-  ( ( U e. V /\ x e. B ) -> ( x ( Hom ` C ) x ) = ( x Func x ) )
21 16 20 eleqtrrd 
 |-  ( ( U e. V /\ x e. B ) -> ( idFunc ` x ) e. ( x ( Hom ` C ) x ) )
22 simpl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> U e. V )
23 eqid 
 |-  ( comp ` C ) = ( comp ` C )
24 simpr1l 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> w e. B )
25 simpr1r 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> x e. B )
26 simpr31 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> f e. ( w ( Hom ` C ) x ) )
27 1 2 22 18 24 25 catchom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( w ( Hom ` C ) x ) = ( w Func x ) )
28 26 27 eleqtrd 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> f e. ( w Func x ) )
29 25 16 syldan 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( idFunc ` x ) e. ( x Func x ) )
30 1 2 22 23 24 25 25 28 29 catcco 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( idFunc ` x ) ( <. w , x >. ( comp ` C ) x ) f ) = ( ( idFunc ` x ) o.func f ) )
31 28 14 cofulid 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( idFunc ` x ) o.func f ) = f )
32 30 31 eqtrd 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( idFunc ` x ) ( <. w , x >. ( comp ` C ) x ) f ) = f )
33 simpr2l 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> y e. B )
34 simpr32 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> g e. ( x ( Hom ` C ) y ) )
35 1 2 22 18 25 33 catchom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( x ( Hom ` C ) y ) = ( x Func y ) )
36 34 35 eleqtrd 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> g e. ( x Func y ) )
37 1 2 22 23 25 25 33 29 36 catcco 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. x , x >. ( comp ` C ) y ) ( idFunc ` x ) ) = ( g o.func ( idFunc ` x ) ) )
38 36 14 cofurid 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g o.func ( idFunc ` x ) ) = g )
39 37 38 eqtrd 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. x , x >. ( comp ` C ) y ) ( idFunc ` x ) ) = g )
40 28 36 cofucl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g o.func f ) e. ( w Func y ) )
41 1 2 22 23 24 25 33 28 36 catcco 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( 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.func f ) )
42 1 2 22 18 24 33 catchom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( w ( Hom ` C ) y ) = ( w Func y ) )
43 40 41 42 3eltr4d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( 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 ) )
44 simpr33 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> h e. ( y ( Hom ` C ) z ) )
45 simpr2r 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> z e. B )
46 1 2 22 18 33 45 catchom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( y ( Hom ` C ) z ) = ( y Func z ) )
47 44 46 eleqtrd 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> h e. ( y Func z ) )
48 28 36 47 cofuass 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h o.func g ) o.func f ) = ( h o.func ( g o.func f ) ) )
49 36 47 cofucl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h o.func g ) e. ( x Func z ) )
50 1 2 22 23 24 25 45 28 49 catcco 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h o.func g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( ( h o.func g ) o.func f ) )
51 1 2 22 23 24 33 45 40 47 catcco 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( 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.func f ) ) = ( h o.func ( g o.func f ) ) )
52 48 50 51 3eqtr4d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h o.func g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( h ( <. w , y >. ( comp ` C ) z ) ( g o.func f ) ) )
53 1 2 22 23 25 33 45 36 47 catcco 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( 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.func g ) )
54 53 oveq1d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( 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.func g ) ( <. w , x >. ( comp ` C ) z ) f ) )
55 41 oveq2d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( 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.func f ) ) )
56 52 54 55 3eqtr4d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( 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 21 32 39 43 56 iscatd2 
 |-  ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( idFunc ` x ) ) ) )