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 )