This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> J e. ( Subcat ` C ) )
subcssc.h 
|- H = ( Homf ` C )
Assertion subcssc 
|- ( ph -> J C_cat H )

Proof

Step Hyp Ref Expression
1 subcixp.1 
 |-  ( ph -> J e. ( Subcat ` C ) )
2 subcssc.h 
 |-  H = ( Homf ` C )
3 eqid 
 |-  ( Id ` C ) = ( Id ` C )
4 eqid 
 |-  ( comp ` C ) = ( comp ` C )
5 subcrcl 
 |-  ( J e. ( Subcat ` C ) -> C e. Cat )
6 1 5 syl 
 |-  ( ph -> C e. Cat )
7 eqidd 
 |-  ( ph -> dom dom J = dom dom J )
8 2 3 4 6 7 issubc 
 |-  ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat H /\ A. x e. dom dom J ( ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. y e. dom dom J A. z e. dom dom J A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) )
9 1 8 mpbid 
 |-  ( ph -> ( J C_cat H /\ A. x e. dom dom J ( ( ( Id ` C ) ` x ) e. ( x J x ) /\ A. y e. dom dom J A. z e. dom dom J A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) )
10 9 simpld 
 |-  ( ph -> J C_cat H )