This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑆 × 𝑆 ) )