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 ⊢ φ → J ∈ Subcat ⁡ C
subcfn.2 ⊢ φ → S = dom ⁡ dom ⁡ J
Assertion subcfn ⊢ φ → J Fn S × S

Proof

Step Hyp Ref Expression
1 subcixp.1 ⊢ φ → J ∈ Subcat ⁡ C
2 subcfn.2 ⊢ φ → S = dom ⁡ dom ⁡ J
3 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
4 1 3 subcssc ⊢ φ → J ⊆ cat Hom 𝑓 ⁡ C
5 4 2 sscfn1 ⊢ φ → J Fn S × S