Theorem catcid

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

	Ref	Expression
Hypotheses	catccatid.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
	catccatid.b	$$⊢B={\mathrm{Base}}_C$$
	catcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	catcid.i	$$⊢I={id}_{\mathrm{func}}\left(X\right)$$
	catcid.u	$$⊢\phi \to U\in V$$
	catcid.x	$$⊢\phi \to X\in B$$
Assertion	catcid	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)=I$$

Proof

Step	Hyp	Ref	Expression
1		catccatid.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		catccatid.b	$$⊢B={\mathrm{Base}}_C$$
3		catcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
4		catcid.i	$$⊢I={id}_{\mathrm{func}}\left(X\right)$$
5		catcid.u	$$⊢\phi \to U\in V$$
6		catcid.x	$$⊢\phi \to X\in B$$
7	1 2	catccatid	$$⊢U\in V\to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(x\in B⟼{id}_{\mathrm{func}}\left(x\right)\right)\right)$$
8	5 7	syl	$$⊢\phi \to \left(C\in \mathrm{Cat}\wedge \mathrm{Id}\left(C\right)=\left(x\in B⟼{id}_{\mathrm{func}}\left(x\right)\right)\right)$$
9	8	simprd	$$⊢\phi \to \mathrm{Id}\left(C\right)=\left(x\in B⟼{id}_{\mathrm{func}}\left(x\right)\right)$$
10	3 9	syl5eq	$$⊢\phi \to \underset{\dot{}}{1}=\left(x\in B⟼{id}_{\mathrm{func}}\left(x\right)\right)$$
11		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
12	11	fveq2d	$$⊢\left(\phi \wedge x=X\right)\to {id}_{\mathrm{func}}\left(x\right)={id}_{\mathrm{func}}\left(X\right)$$
13		fvexd	$$⊢\phi \to {id}_{\mathrm{func}}\left(X\right)\in \mathrm{V}$$
14	10 12 6 13	fvmptd	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={id}_{\mathrm{func}}\left(X\right)$$
15	14 4	eqtr4di	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)=I$$