Theorem subccat

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

	Ref	Expression
Hypotheses	subccat.1	|- D = ( C |`cat J )
	subccat.j	|- ( ph -> J e. ( Subcat ` C ) )
Assertion	subccat	|- ( ph -> D e. Cat )

Proof

Step	Hyp	Ref	Expression
1		subccat.1	|- D = ( C |`cat J )
2		subccat.j	|- ( ph -> J e. ( Subcat ` C ) )
3		eqidd	|- ( ph -> dom dom J = dom dom J )
4	2 3	subcfn	|- ( ph -> J Fn ( dom dom J X. dom dom J ) )
5		eqid	|- ( Id ` C ) = ( Id ` C )
6	1 2 4 5	subccatid	|- ( ph -> ( D e. Cat /\ ( Id ` D ) = ( x e. dom dom J |-> ( ( Id ` C ) ` x ) ) ) )
7	6	simpld	|- ( ph -> D e. Cat )