Metamath Proof Explorer


Theorem subccat

Description: A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subccat.1 𝐷 = ( 𝐶cat 𝐽 )
subccat.j ( 𝜑𝐽 ∈ ( Subcat ‘ 𝐶 ) )
Assertion subccat ( 𝜑𝐷 ∈ Cat )

Proof

Step Hyp Ref Expression
1 subccat.1 𝐷 = ( 𝐶cat 𝐽 )
2 subccat.j ( 𝜑𝐽 ∈ ( Subcat ‘ 𝐶 ) )
3 eqidd ( 𝜑 → dom dom 𝐽 = dom dom 𝐽 )
4 2 3 subcfn ( 𝜑𝐽 Fn ( dom dom 𝐽 × dom dom 𝐽 ) )
5 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
6 1 2 4 5 subccatid ( 𝜑 → ( 𝐷 ∈ Cat ∧ ( Id ‘ 𝐷 ) = ( 𝑥 ∈ dom dom 𝐽 ↦ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ) )
7 6 simpld ( 𝜑𝐷 ∈ Cat )