Metamath Proof Explorer

Theorem fuccatid

Description: The functor category is a category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses fuccat.q 
|- Q = ( C FuncCat D )
fuccat.r 
|- ( ph -> C e. Cat )
fuccat.s 
|- ( ph -> D e. Cat )
fuccatid.1 
|- .1. = ( Id ` D )
Assertion fuccatid 
|- ( ph -> ( Q e. Cat /\ ( Id ` Q ) = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fuccat.q 
 |-  Q = ( C FuncCat D )
2 fuccat.r 
 |-  ( ph -> C e. Cat )
3 fuccat.s 
 |-  ( ph -> D e. Cat )
4 fuccatid.1 
 |-  .1. = ( Id ` D )
5 1 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
6 5 a1i 
 |-  ( ph -> ( C Func D ) = ( Base ` Q ) )
7 eqid 
 |-  ( C Nat D ) = ( C Nat D )
8 1 7 fuchom 
 |-  ( C Nat D ) = ( Hom ` Q )
9 8 a1i 
 |-  ( ph -> ( C Nat D ) = ( Hom ` Q ) )
10 eqidd 
 |-  ( ph -> ( comp ` Q ) = ( comp ` Q ) )
11 1 ovexi 
 |-  Q e. _V
12 11 a1i 
 |-  ( ph -> Q e. _V )
13 biid 
 |-  ( ( ( e e. ( C Func D ) /\ f e. ( C Func D ) ) /\ ( g e. ( C Func D ) /\ h e. ( C Func D ) ) /\ ( r e. ( e ( C Nat D ) f ) /\ s e. ( f ( C Nat D ) g ) /\ t e. ( g ( C Nat D ) h ) ) ) <-> ( ( e e. ( C Func D ) /\ f e. ( C Func D ) ) /\ ( g e. ( C Func D ) /\ h e. ( C Func D ) ) /\ ( r e. ( e ( C Nat D ) f ) /\ s e. ( f ( C Nat D ) g ) /\ t e. ( g ( C Nat D ) h ) ) ) )
14 simpr 
 |-  ( ( ph /\ f e. ( C Func D ) ) -> f e. ( C Func D ) )
15 1 7 4 14 fucidcl 
 |-  ( ( ph /\ f e. ( C Func D ) ) -> ( .1. o. ( 1st ` f ) ) e. ( f ( C Nat D ) f ) )
16 eqid 
 |-  ( comp ` Q ) = ( comp ` Q )
17 simpr31 
 |-  ( ( ph /\ ( ( e e. ( C Func D ) /\ f e. ( C Func D ) ) /\ ( g e. ( C Func D ) /\ h e. ( C Func D ) ) /\ ( r e. ( e ( C Nat D ) f ) /\ s e. ( f ( C Nat D ) g ) /\ t e. ( g ( C Nat D ) h ) ) ) ) -> r e. ( e ( C Nat D ) f ) )
18 1 7 16 4 17 fuclid 
 |-  ( ( ph /\ ( ( e e. ( C Func D ) /\ f e. ( C Func D ) ) /\ ( g e. ( C Func D ) /\ h e. ( C Func D ) ) /\ ( r e. ( e ( C Nat D ) f ) /\ s e. ( f ( C Nat D ) g ) /\ t e. ( g ( C Nat D ) h ) ) ) ) -> ( ( .1. o. ( 1st ` f ) ) ( <. e , f >. ( comp ` Q ) f ) r ) = r )
19 simpr32 
 |-  ( ( ph /\ ( ( e e. ( C Func D ) /\ f e. ( C Func D ) ) /\ ( g e. ( C Func D ) /\ h e. ( C Func D ) ) /\ ( r e. ( e ( C Nat D ) f ) /\ s e. ( f ( C Nat D ) g ) /\ t e. ( g ( C Nat D ) h ) ) ) ) -> s e. ( f ( C Nat D ) g ) )
20 1 7 16 4 19 fucrid 
 |-  ( ( ph /\ ( ( e e. ( C Func D ) /\ f e. ( C Func D ) ) /\ ( g e. ( C Func D ) /\ h e. ( C Func D ) ) /\ ( r e. ( e ( C Nat D ) f ) /\ s e. ( f ( C Nat D ) g ) /\ t e. ( g ( C Nat D ) h ) ) ) ) -> ( s ( <. f , f >. ( comp ` Q ) g ) ( .1. o. ( 1st ` f ) ) ) = s )
21 1 7 16 17 19 fuccocl 
 |-  ( ( ph /\ ( ( e e. ( C Func D ) /\ f e. ( C Func D ) ) /\ ( g e. ( C Func D ) /\ h e. ( C Func D ) ) /\ ( r e. ( e ( C Nat D ) f ) /\ s e. ( f ( C Nat D ) g ) /\ t e. ( g ( C Nat D ) h ) ) ) ) -> ( s ( <. e , f >. ( comp ` Q ) g ) r ) e. ( e ( C Nat D ) g ) )
22 simpr33 
 |-  ( ( ph /\ ( ( e e. ( C Func D ) /\ f e. ( C Func D ) ) /\ ( g e. ( C Func D ) /\ h e. ( C Func D ) ) /\ ( r e. ( e ( C Nat D ) f ) /\ s e. ( f ( C Nat D ) g ) /\ t e. ( g ( C Nat D ) h ) ) ) ) -> t e. ( g ( C Nat D ) h ) )
23 1 7 16 17 19 22 fucass 
 |-  ( ( ph /\ ( ( e e. ( C Func D ) /\ f e. ( C Func D ) ) /\ ( g e. ( C Func D ) /\ h e. ( C Func D ) ) /\ ( r e. ( e ( C Nat D ) f ) /\ s e. ( f ( C Nat D ) g ) /\ t e. ( g ( C Nat D ) h ) ) ) ) -> ( ( t ( <. f , g >. ( comp ` Q ) h ) s ) ( <. e , f >. ( comp ` Q ) h ) r ) = ( t ( <. e , g >. ( comp ` Q ) h ) ( s ( <. e , f >. ( comp ` Q ) g ) r ) ) )
24 6 9 10 12 13 15 18 20 21 23 iscatd2 
 |-  ( ph -> ( Q e. Cat /\ ( Id ` Q ) = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) ) )