Theorem subcid

Description: The identity in a subcategory is the same as the original category. (Contributed by Mario Carneiro, 4-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		subccat.1	|- D = ( C |`cat J )
2		subccat.j	|- ( ph -> J e. ( Subcat ` C ) )
3		subccatid.1	|- ( ph -> J Fn ( S X. S ) )
4		subccatid.2	|- .1. = ( Id ` C )
5		subcid.x	|- ( ph -> X e. S )
6	1 2 3 4	subccatid	|- ( ph -> ( D e. Cat /\ ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) ) )
7	6	simprd	|- ( ph -> ( Id ` D ) = ( x e. S |-> ( .1. ` x ) ) )
8		simpr	|- ( ( ph /\ x = X ) -> x = X )
9	8	fveq2d	|- ( ( ph /\ x = X ) -> ( .1. ` x ) = ( .1. ` X ) )
10		fvexd	|- ( ph -> ( .1. ` X ) e. _V )
11	7 9 5 10	fvmptd	|- ( ph -> ( ( Id ` D ) ` X ) = ( .1. ` X ) )
12	11	eqcomd	|- ( ph -> ( .1. ` X ) = ( ( Id ` D ) ` X ) )