Step |
Hyp |
Ref |
Expression |
1 |
|
subcss1.1 |
|- ( ph -> J e. ( Subcat ` C ) ) |
2 |
|
subcss1.2 |
|- ( ph -> J Fn ( S X. S ) ) |
3 |
|
subcss2.h |
|- H = ( Hom ` C ) |
4 |
|
subcss2.x |
|- ( ph -> X e. S ) |
5 |
|
subcss2.y |
|- ( ph -> Y e. S ) |
6 |
|
eqid |
|- ( Homf ` C ) = ( Homf ` C ) |
7 |
1 6
|
subcssc |
|- ( ph -> J C_cat ( Homf ` C ) ) |
8 |
2 7 4 5
|
ssc2 |
|- ( ph -> ( X J Y ) C_ ( X ( Homf ` C ) Y ) ) |
9 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
10 |
1 2 9
|
subcss1 |
|- ( ph -> S C_ ( Base ` C ) ) |
11 |
10 4
|
sseldd |
|- ( ph -> X e. ( Base ` C ) ) |
12 |
10 5
|
sseldd |
|- ( ph -> Y e. ( Base ` C ) ) |
13 |
6 9 3 11 12
|
homfval |
|- ( ph -> ( X ( Homf ` C ) Y ) = ( X H Y ) ) |
14 |
8 13
|
sseqtrd |
|- ( ph -> ( X J Y ) C_ ( X H Y ) ) |