Metamath Proof Explorer

Theorem subcrcl

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

Ref Expression
Assertion subcrcl 
|- ( H e. ( Subcat ` C ) -> C e. Cat )

Proof

Step Hyp Ref Expression
1 df-subc 
 |-  Subcat = ( c e. Cat |-> { h | ( h C_cat ( Homf ` c ) /\ [. dom dom h / s ]. A. x e. s ( ( ( Id ` c ) ` x ) e. ( x h x ) /\ A. y e. s A. z e. s A. f e. ( x h y ) A. g e. ( y h z ) ( g ( <. x , y >. ( comp ` c ) z ) f ) e. ( x h z ) ) ) } )
2 1 mptrcl 
 |-  ( H e. ( Subcat ` C ) -> C e. Cat )