Metamath Proof Explorer


Theorem subcssc

Description: An element in the set of subcategories is a subset of the category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses subcixp.1 φJSubcatC
subcssc.h H=Hom𝑓C
Assertion subcssc φJcatH

Proof

Step Hyp Ref Expression
1 subcixp.1 φJSubcatC
2 subcssc.h H=Hom𝑓C
3 eqid IdC=IdC
4 eqid compC=compC
5 subcrcl JSubcatCCCat
6 1 5 syl φCCat
7 eqidd φdomdomJ=domdomJ
8 2 3 4 6 7 issubc φJSubcatCJcatHxdomdomJIdCxxJxydomdomJzdomdomJfxJygyJzgxycompCzfxJz
9 1 8 mpbid φJcatHxdomdomJIdCxxJxydomdomJzdomdomJfxJygyJzgxycompCzfxJz
10 9 simpld φJcatH