Theorem setcid

Description: The identity arrow in the category of sets is the identity function. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	setccat.c	|- C = ( SetCat ` U )
	setcid.o	|- .1. = ( Id ` C )
	setcid.u	|- ( ph -> U e. V )
	setcid.x	|- ( ph -> X e. U )
Assertion	setcid	|- ( ph -> ( .1. ` X ) = ( _I |` X ) )

Proof

Step	Hyp	Ref	Expression
1		setccat.c	|- C = ( SetCat ` U )
2		setcid.o	|- .1. = ( Id ` C )
3		setcid.u	|- ( ph -> U e. V )
4		setcid.x	|- ( ph -> X e. U )
5	1	setccatid	|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` x ) ) ) )
6	3 5	syl	|- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( x e. U |-> ( _I |` x ) ) ) )
7	6	simprd	|- ( ph -> ( Id ` C ) = ( x e. U |-> ( _I |` x ) ) )
8	2 7	eqtrid	|- ( ph -> .1. = ( x e. U |-> ( _I |` x ) ) )
9		simpr	|- ( ( ph /\ x = X ) -> x = X )
10	9	reseq2d	|- ( ( ph /\ x = X ) -> ( _I |` x ) = ( _I |` X ) )
11	4	resiexd	|- ( ph -> ( _I |` X ) e. _V )
12	8 10 4 11	fvmptd	|- ( ph -> ( .1. ` X ) = ( _I |` X ) )