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 ) ) ) ) )