| 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 |
|
1nn0 |
|- 1 e. NN0 |
| 9 |
|
4nn |
|- 4 e. NN |
| 10 |
8 9
|
decnncl |
|- ; 1 4 e. NN |
| 11 |
10
|
nnrei |
|- ; 1 4 e. RR |
| 12 |
|
4nn0 |
|- 4 e. NN0 |
| 13 |
|
5nn |
|- 5 e. NN |
| 14 |
|
4lt5 |
|- 4 < 5 |
| 15 |
8 12 13 14
|
declt |
|- ; 1 4 < ; 1 5 |
| 16 |
11 15
|
gtneii |
|- ; 1 5 =/= ; 1 4 |
| 17 |
|
ccondx |
|- ( comp ` ndx ) = ; 1 5 |
| 18 |
|
homndx |
|- ( Hom ` ndx ) = ; 1 4 |
| 19 |
17 18
|
neeq12i |
|- ( ( comp ` ndx ) =/= ( Hom ` ndx ) <-> ; 1 5 =/= ; 1 4 ) |
| 20 |
16 19
|
mpbir |
|- ( comp ` ndx ) =/= ( Hom ` ndx ) |
| 21 |
7 20
|
setsnid |
|- ( comp ` ( C |`s S ) ) = ( comp ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) |
| 22 |
2
|
fvexi |
|- B e. _V |
| 23 |
22
|
ssex |
|- ( S C_ B -> S e. _V ) |
| 24 |
5 23
|
syl |
|- ( ph -> S e. _V ) |
| 25 |
|
eqid |
|- ( C |`s S ) = ( C |`s S ) |
| 26 |
25 6
|
ressco |
|- ( S e. _V -> .x. = ( comp ` ( C |`s S ) ) ) |
| 27 |
24 26
|
syl |
|- ( ph -> .x. = ( comp ` ( C |`s S ) ) ) |
| 28 |
1 3 24 4
|
rescval2 |
|- ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) |
| 29 |
28
|
fveq2d |
|- ( ph -> ( comp ` D ) = ( comp ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) ) |
| 30 |
21 27 29
|
3eqtr4a |
|- ( ph -> .x. = ( comp ` D ) ) |