Metamath Proof Explorer


Theorem subcrcl

Description: Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion subcrcl HSubcatCCCat

Proof

Step Hyp Ref Expression
1 df-subc Subcat=cCath|hcatHom𝑓c[˙domdomh/s]˙xsIdcxxhxyszsfxhygyhzgxycompczfxhz
2 1 mptrcl HSubcatCCCat