| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rescbas.d |
|- D = ( C |`cat H ) |
| 2 |
|
rescbas.b |
|- B = ( Base ` C ) |
| 3 |
|
rescbas.c |
|- ( ph -> C e. V ) |
| 4 |
|
rescbas.h |
|- ( ph -> H Fn ( S X. S ) ) |
| 5 |
|
rescbas.s |
|- ( ph -> S C_ B ) |
| 6 |
|
rescco.o |
|- .x. = ( comp ` C ) |
| 7 |
|
ccoid |
|- comp = Slot ( comp ` ndx ) |
| 8 |
|
slotsbhcdif |
|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) |
| 9 |
|
simp3 |
|- ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( Hom ` ndx ) =/= ( comp ` ndx ) ) |
| 10 |
9
|
necomd |
|- ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( comp ` ndx ) =/= ( Hom ` ndx ) ) |
| 11 |
8 10
|
ax-mp |
|- ( comp ` ndx ) =/= ( Hom ` ndx ) |
| 12 |
7 11
|
setsnid |
|- ( comp ` ( C |`s S ) ) = ( comp ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) |
| 13 |
2
|
fvexi |
|- B e. _V |
| 14 |
13
|
ssex |
|- ( S C_ B -> S e. _V ) |
| 15 |
5 14
|
syl |
|- ( ph -> S e. _V ) |
| 16 |
|
eqid |
|- ( C |`s S ) = ( C |`s S ) |
| 17 |
16 6
|
ressco |
|- ( S e. _V -> .x. = ( comp ` ( C |`s S ) ) ) |
| 18 |
15 17
|
syl |
|- ( ph -> .x. = ( comp ` ( C |`s S ) ) ) |
| 19 |
1 3 15 4
|
rescval2 |
|- ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) |
| 20 |
19
|
fveq2d |
|- ( ph -> ( comp ` D ) = ( comp ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) ) |
| 21 |
12 18 20
|
3eqtr4a |
|- ( ph -> .x. = ( comp ` D ) ) |