Metamath Proof Explorer


Theorem subcfn

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 ) )

Proof

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 ) )