Description: An element in the set of subcategories is a binary function. (Contributed by Mario Carneiro, 4-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subcixp.1 | |- ( ph -> J e. ( Subcat ` C ) ) |
|
subcfn.2 | |- ( ph -> S = dom dom J ) |
||
Assertion | subcfn | |- ( ph -> J Fn ( S X. S ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subcixp.1 | |- ( ph -> J e. ( Subcat ` C ) ) |
|
2 | subcfn.2 | |- ( ph -> S = dom dom J ) |
|
3 | eqid | |- ( Homf ` C ) = ( Homf ` C ) |
|
4 | 1 3 | subcssc | |- ( ph -> J C_cat ( Homf ` C ) ) |
5 | 4 2 | sscfn1 | |- ( ph -> J Fn ( S X. S ) ) |