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=\mathrm{SetCat}\left(U\right)$$
	setcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	setcid.u	$$⊢\phi \to U\in V$$
	setcid.x	$$⊢\phi \to X\in U$$
Assertion	setcid	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_X$$

Proof

Step	Hyp	Ref	Expression
1		setccat.c	$$⊢C=\mathrm{SetCat}\left(U\right)$$
2		setcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
3		setcid.u	$$⊢\phi \to U\in V$$
4		setcid.x	$$⊢\phi \to X\in U$$
5	1	setccatid	$$⊢U\in V\to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(x\in U⟼{\mathrm{I}\upharpoonright }_x\right)\right)$$
6	3 5	syl	$$⊢\phi \to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(x\in U⟼{\mathrm{I}\upharpoonright }_x\right)\right)$$
7	6	simprd	$$⊢\phi \to \mathrm{Id}\left(C\right)=\left(x\in U⟼{\mathrm{I}\upharpoonright }_x\right)$$
8	2 7	syl5eq	$$⊢\phi \to \underset{\dot{}}{1}=\left(x\in U⟼{\mathrm{I}\upharpoonright }_x\right)$$
9		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
10	9	reseq2d	$$⊢\left(\phi \wedge x=X\right)\to {\mathrm{I}\upharpoonright }_x={\mathrm{I}\upharpoonright }_X$$
11	4	resiexd	$$⊢\phi \to {\mathrm{I}\upharpoonright }_X\in \mathrm{V}$$
12	8 10 4 11	fvmptd	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_X$$