Metamath Proof Explorer


Theorem subcss1

Description: The objects of a subcategory are a subset of the objects of the original. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subcss1.1 φJSubcatC
subcss1.2 φJFnS×S
subcss1.b B=BaseC
Assertion subcss1 φSB

Proof

Step Hyp Ref Expression
1 subcss1.1 φJSubcatC
2 subcss1.2 φJFnS×S
3 subcss1.b B=BaseC
4 eqid Hom𝑓C=Hom𝑓C
5 4 3 homffn Hom𝑓CFnB×B
6 5 a1i φHom𝑓CFnB×B
7 1 4 subcssc φJcatHom𝑓C
8 2 6 7 ssc1 φSB