Theorem estrcid

Description: The identity arrow in the category of extensible structures is the identity function of base sets. (Contributed by AV, 8-Mar-2020)

	Ref	Expression
Hypotheses	estrccat.c	|- C = ( ExtStrCat ` U )
	estrcid.o	|- .1. = ( Id ` C )
	estrcid.u	|- ( ph -> U e. V )
	estrcid.x	|- ( ph -> X e. U )
Assertion	estrcid	|- ( ph -> ( .1. ` X ) = ( _I |` ( Base ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		estrccat.c	|- C = ( ExtStrCat ` U )
2		estrcid.o	|- .1. = ( Id ` C )
3		estrcid.u	|- ( ph -> U e. V )
4		estrcid.x	|- ( ph -> X e. U )
5	1	estrccatid	|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) )
6	3 5	syl	|- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) ) )
7	6	simprd	|- ( ph -> ( Id ` C ) = ( x e. U |-> ( _I |` ( Base ` x ) ) ) )
8	2 7	eqtrid	|- ( ph -> .1. = ( x e. U |-> ( _I |` ( Base ` x ) ) ) )
9		fveq2	|- ( x = X -> ( Base ` x ) = ( Base ` X ) )
10	9	reseq2d	|- ( x = X -> ( _I |` ( Base ` x ) ) = ( _I |` ( Base ` X ) ) )
11	10	adantl	|- ( ( ph /\ x = X ) -> ( _I |` ( Base ` x ) ) = ( _I |` ( Base ` X ) ) )
12		fvexd	|- ( ph -> ( Base ` X ) e. _V )
13	12	resiexd	|- ( ph -> ( _I |` ( Base ` X ) ) e. _V )
14	8 11 4 13	fvmptd	|- ( ph -> ( .1. ` X ) = ( _I |` ( Base ` X ) ) )