Metamath Proof Explorer


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 )