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