Theorem subcidcl

Description: The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	subcidcl.j	|- ( ph -> J e. ( Subcat ` C ) )
	subcidcl.2	|- ( ph -> J Fn ( S X. S ) )
	subcidcl.x	|- ( ph -> X e. S )
	subcidcl.1	|- .1. = ( Id ` C )
Assertion	subcidcl	|- ( ph -> ( .1. ` X ) e. ( X J X ) )

Proof

Step	Hyp	Ref	Expression
1		subcidcl.j	|- ( ph -> J e. ( Subcat ` C ) )
2		subcidcl.2	|- ( ph -> J Fn ( S X. S ) )
3		subcidcl.x	|- ( ph -> X e. S )
4		subcidcl.1	|- .1. = ( Id ` C )
5		fveq2	|- ( x = X -> ( .1. ` x ) = ( .1. ` X ) )
6		id	|- ( x = X -> x = X )
7	6 6	oveq12d	|- ( x = X -> ( x J x ) = ( X J X ) )
8	5 7	eleq12d	|- ( x = X -> ( ( .1. ` x ) e. ( x J x ) <-> ( .1. ` X ) e. ( X J X ) ) )
9		eqid	|- ( Homf ` C ) = ( Homf ` C )
10		eqid	|- ( comp ` C ) = ( comp ` C )
11		subcrcl	|- ( J e. ( Subcat ` C ) -> C e. Cat )
12	1 11	syl	|- ( ph -> C e. Cat )
13	9 4 10 12 2	issubc2	|- ( ph -> ( J e. ( Subcat ` C ) <-> ( J C_cat ( Homf ` C ) /\ A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) ) )
14	1 13	mpbid	|- ( ph -> ( J C_cat ( Homf ` C ) /\ A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) ) )
15		simpl	|- ( ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) -> ( .1. ` x ) e. ( x J x ) )
16	15	ralimi	|- ( A. x e. S ( ( .1. ` x ) e. ( x J x ) /\ A. y e. S A. z e. S A. f e. ( x J y ) A. g e. ( y J z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x J z ) ) -> A. x e. S ( .1. ` x ) e. ( x J x ) )
17	14 16	simpl2im	|- ( ph -> A. x e. S ( .1. ` x ) e. ( x J x ) )
18	8 17 3	rspcdva	|- ( ph -> ( .1. ` X ) e. ( X J X ) )