Step |
Hyp |
Ref |
Expression |
1 |
|
fucid.q |
|- Q = ( C FuncCat D ) |
2 |
|
fucid.i |
|- I = ( Id ` Q ) |
3 |
|
fucid.1 |
|- .1. = ( Id ` D ) |
4 |
|
fucid.f |
|- ( ph -> F e. ( C Func D ) ) |
5 |
|
funcrcl |
|- ( F e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) ) |
6 |
4 5
|
syl |
|- ( ph -> ( C e. Cat /\ D e. Cat ) ) |
7 |
6
|
simpld |
|- ( ph -> C e. Cat ) |
8 |
6
|
simprd |
|- ( ph -> D e. Cat ) |
9 |
1 7 8 3
|
fuccatid |
|- ( ph -> ( Q e. Cat /\ ( Id ` Q ) = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) ) ) |
10 |
9
|
simprd |
|- ( ph -> ( Id ` Q ) = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) ) |
11 |
2 10
|
eqtrid |
|- ( ph -> I = ( f e. ( C Func D ) |-> ( .1. o. ( 1st ` f ) ) ) ) |
12 |
|
simpr |
|- ( ( ph /\ f = F ) -> f = F ) |
13 |
12
|
fveq2d |
|- ( ( ph /\ f = F ) -> ( 1st ` f ) = ( 1st ` F ) ) |
14 |
13
|
coeq2d |
|- ( ( ph /\ f = F ) -> ( .1. o. ( 1st ` f ) ) = ( .1. o. ( 1st ` F ) ) ) |
15 |
3
|
fvexi |
|- .1. e. _V |
16 |
|
fvex |
|- ( 1st ` F ) e. _V |
17 |
15 16
|
coex |
|- ( .1. o. ( 1st ` F ) ) e. _V |
18 |
17
|
a1i |
|- ( ph -> ( .1. o. ( 1st ` F ) ) e. _V ) |
19 |
11 14 4 18
|
fvmptd |
|- ( ph -> ( I ` F ) = ( .1. o. ( 1st ` F ) ) ) |