Metamath Proof Explorer

Theorem estrccatid

Description: Lemma for estrccat . (Contributed by AV, 8-Mar-2020)

Ref Expression
Hypothesis estrccat.c 
|- C = ( ExtStrCat ` U )
Assertion estrccatid 
|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 estrccat.c 
 |-  C = ( ExtStrCat ` U )
2 id 
 |-  ( U e. V -> U e. V )
3 1 2 estrcbas 
 |-  ( 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 |` ( Base ` x ) ) : ( Base ` x ) -1-1-onto-> ( Base ` x )
10 f1of 
 |-  ( ( _I |` ( Base ` x ) ) : ( Base ` x ) -1-1-onto-> ( Base ` x ) -> ( _I |` ( Base ` x ) ) : ( Base ` x ) --> ( Base ` x ) )
11 9 10 mp1i 
 |-  ( ( U e. V /\ x e. U ) -> ( _I |` ( Base ` x ) ) : ( Base ` x ) --> ( Base ` 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 eqid 
 |-  ( Base ` x ) = ( Base ` x )
16 1 12 13 14 14 15 15 elestrchom 
 |-  ( ( U e. V /\ x e. U ) -> ( ( _I |` ( Base ` x ) ) e. ( x ( Hom ` C ) x ) <-> ( _I |` ( Base ` x ) ) : ( Base ` x ) --> ( Base ` x ) ) )
17 11 16 mpbird 
 |-  ( ( U e. V /\ x e. U ) -> ( _I |` ( Base ` x ) ) e. ( x ( Hom ` C ) x ) )
18 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 )
19 eqid 
 |-  ( comp ` C ) = ( comp ` C )
20 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 )
21 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 )
22 eqid 
 |-  ( Base ` w ) = ( Base ` w )
23 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 ) )
24 1 18 13 20 21 22 15 elestrchom 
 |-  ( ( 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 : ( Base ` w ) --> ( Base ` x ) ) )
25 23 24 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 : ( Base ` w ) --> ( Base ` x ) )
26 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 |` ( Base ` x ) ) : ( Base ` x ) --> ( Base ` x ) )
27 1 18 19 20 21 21 22 15 15 25 26 estrcco 
 |-  ( ( 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 |` ( Base ` x ) ) ( <. w , x >. ( comp ` C ) x ) f ) = ( ( _I |` ( Base ` x ) ) o. f ) )
28 fcoi2 
 |-  ( f : ( Base ` w ) --> ( Base ` x ) -> ( ( _I |` ( Base ` x ) ) o. f ) = f )
29 25 28 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 |` ( Base ` x ) ) o. f ) = f )
30 27 29 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 |` ( Base ` x ) ) ( <. w , x >. ( comp ` C ) x ) f ) = f )
31 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 )
32 eqid 
 |-  ( Base ` y ) = ( Base ` y )
33 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 ) )
34 1 18 13 21 31 15 32 elestrchom 
 |-  ( ( 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 : ( Base ` x ) --> ( Base ` y ) ) )
35 33 34 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 : ( Base ` x ) --> ( Base ` y ) )
36 1 18 19 21 21 31 15 15 32 26 35 estrcco 
 |-  ( ( 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 |` ( Base ` x ) ) ) = ( g o. ( _I |` ( Base ` x ) ) ) )
37 fcoi1 
 |-  ( g : ( Base ` x ) --> ( Base ` y ) -> ( g o. ( _I |` ( Base ` x ) ) ) = g )
38 35 37 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 |` ( Base ` x ) ) ) = g )
39 36 38 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 |` ( Base ` x ) ) ) = g )
40 1 18 19 20 21 31 22 15 32 25 35 estrcco 
 |-  ( ( 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 ) )
41 fco 
 |-  ( ( g : ( Base ` x ) --> ( Base ` y ) /\ f : ( Base ` w ) --> ( Base ` x ) ) -> ( g o. f ) : ( Base ` w ) --> ( Base ` y ) )
42 35 25 41 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 ) : ( Base ` w ) --> ( Base ` y ) )
43 1 18 13 20 31 22 32 elestrchom 
 |-  ( ( 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 ) : ( Base ` w ) --> ( Base ` y ) ) )
44 42 43 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 ) )
45 40 44 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 ) )
46 coass 
 |-  ( ( h o. g ) o. f ) = ( h o. ( g o. f ) )
47 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 )
48 eqid 
 |-  ( Base ` z ) = ( Base ` z )
49 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 ) )
50 1 18 13 31 47 32 48 elestrchom 
 |-  ( ( 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 : ( Base ` y ) --> ( Base ` z ) ) )
51 49 50 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 : ( Base ` y ) --> ( Base ` z ) )
52 fco 
 |-  ( ( h : ( Base ` y ) --> ( Base ` z ) /\ g : ( Base ` x ) --> ( Base ` y ) ) -> ( h o. g ) : ( Base ` x ) --> ( Base ` z ) )
53 51 35 52 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 ) : ( Base ` x ) --> ( Base ` z ) )
54 1 18 19 20 21 47 22 15 48 25 53 estrcco 
 |-  ( ( 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 ) )
55 1 18 19 20 31 47 22 32 48 42 51 estrcco 
 |-  ( ( 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 ) ) )
56 46 54 55 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 ) ) )
57 1 18 19 21 31 47 15 32 48 35 51 estrcco 
 |-  ( ( 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 ) )
58 57 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 ) )
59 40 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 ) ) )
60 56 58 59 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 ) ) )
61 3 4 5 7 8 17 30 39 45 60 iscatd2 
 |-  ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) )