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 )