Theorem idfu1st

Description: Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	idfuval.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	idfuval.b	$$⊢B={\mathrm{Base}}_C$$
	idfuval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
Assertion	idfu1st	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		idfuval.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
2		idfuval.b	$$⊢B={\mathrm{Base}}_C$$
3		idfuval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
5	1 2 3 4	idfuval	$$⊢\phi \to I=⟨{\mathrm{I}\upharpoonright }_B,\left(z\in \left(B\times B\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(C\right)\left(z\right)}\right)⟩$$
6	5	fveq2d	$$⊢\phi \to 1^{st}\left(I\right)=1^{st}\left(⟨{\mathrm{I}\upharpoonright }_B,\left(z\in \left(B\times B\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(C\right)\left(z\right)}\right)⟩\right)$$
7	2	fvexi	$$⊢B\in \mathrm{V}$$
8		resiexg	$$⊢B\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_B\in \mathrm{V}$$
9	7 8	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_B\in \mathrm{V}$$
10	7 7	xpex	$$⊢B\times B\in \mathrm{V}$$
11	10	mptex	$$⊢\left(z\in \left(B\times B\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(C\right)\left(z\right)}\right)\in \mathrm{V}$$
12	9 11	op1st	$$⊢1^{st}\left(⟨{\mathrm{I}\upharpoonright }_B,\left(z\in \left(B\times B\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(C\right)\left(z\right)}\right)⟩\right)={\mathrm{I}\upharpoonright }_B$$
13	6 12	syl6eq	$$⊢\phi \to 1^{st}\left(I\right)={\mathrm{I}\upharpoonright }_B$$