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