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 ( 𝜑𝐽 ∈ ( Subcat ‘ 𝐶 ) )
subcfn.2 ( 𝜑𝑆 = dom dom 𝐽 )
Assertion subcfn ( 𝜑𝐽 Fn ( 𝑆 × 𝑆 ) )

Proof

Step Hyp Ref Expression
1 subcixp.1 ( 𝜑𝐽 ∈ ( Subcat ‘ 𝐶 ) )
2 subcfn.2 ( 𝜑𝑆 = dom dom 𝐽 )
3 eqid ( Homf𝐶 ) = ( Homf𝐶 )
4 1 3 subcssc ( 𝜑𝐽cat ( Homf𝐶 ) )
5 4 2 sscfn1 ( 𝜑𝐽 Fn ( 𝑆 × 𝑆 ) )