Step |
Hyp |
Ref |
Expression |
1 |
|
subccat.1 |
|- D = ( C |`cat J ) |
2 |
|
subccat.j |
|- ( ph -> J e. ( Subcat ` C ) ) |
3 |
|
subccatid.1 |
|- ( ph -> J Fn ( S X. S ) ) |
4 |
|
subccatid.2 |
|- .1. = ( Id ` C ) |
5 |
|
subcid.x |
|- ( ph -> X e. S ) |
6 |
1 2 3 4
|
subccatid |
|- ( ph -> ( D e. Cat /\ ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) ) ) |
7 |
6
|
simprd |
|- ( ph -> ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) ) |
8 |
|
simpr |
|- ( ( ph /\ x = X ) -> x = X ) |
9 |
8
|
fveq2d |
|- ( ( ph /\ x = X ) -> ( .1. ` x ) = ( .1. ` X ) ) |
10 |
|
fvexd |
|- ( ph -> ( .1. ` X ) e. _V ) |
11 |
7 9 5 10
|
fvmptd |
|- ( ph -> ( ( Id ` D ) ` X ) = ( .1. ` X ) ) |
12 |
11
|
eqcomd |
|- ( ph -> ( .1. ` X ) = ( ( Id ` D ) ` X ) ) |