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 ) |
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 ) |