Theorem fucid

Description: The identity morphism in the functor category. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	fucid.q	$$⊢Q=C\mathrm{FuncCat}D$$
	fucid.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
	fucid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(D\right)$$
	fucid.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
Assertion	fucid	$$⊢\phi \to I\left(F\right)=\underset{\dot{}}{1}\circ 1^{st}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		fucid.q	$$⊢Q=C\mathrm{FuncCat}D$$
2		fucid.i	$$⊢I=\mathrm{Id}\left(Q\right)$$
3		fucid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(D\right)$$
4		fucid.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
5		funcrcl	$$⊢F\in \left(C\mathrm{Func}D\right)\to \left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)$$
6	4 5	syl	$$⊢\phi \to \left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)$$
7	6	simpld	$$⊢\phi \to C\in \mathrm{Cat}$$
8	6	simprd	$$⊢\phi \to D\in \mathrm{Cat}$$
9	1 7 8 3	fuccatid	$$⊢\phi \to \left(Q\in \mathrm{Cat}\wedge \mathrm{Id}\left(Q\right)=\left(f\in \left(C\mathrm{Func}D\right)⟼\underset{\dot{}}{1}\circ 1^{st}\left(f\right)\right)\right)$$
10	9	simprd	$$⊢\phi \to \mathrm{Id}\left(Q\right)=\left(f\in \left(C\mathrm{Func}D\right)⟼\underset{\dot{}}{1}\circ 1^{st}\left(f\right)\right)$$
11	2 10	syl5eq	$$⊢\phi \to I=\left(f\in \left(C\mathrm{Func}D\right)⟼\underset{\dot{}}{1}\circ 1^{st}\left(f\right)\right)$$
12		simpr	$$⊢\left(\phi \wedge f=F\right)\to f=F$$
13	12	fveq2d	$$⊢\left(\phi \wedge f=F\right)\to 1^{st}\left(f\right)=1^{st}\left(F\right)$$
14	13	coeq2d	$$⊢\left(\phi \wedge f=F\right)\to \underset{\dot{}}{1}\circ 1^{st}\left(f\right)=\underset{\dot{}}{1}\circ 1^{st}\left(F\right)$$
15	3	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
16		fvex	$$⊢1^{st}\left(F\right)\in \mathrm{V}$$
17	15 16	coex	$$⊢\underset{\dot{}}{1}\circ 1^{st}\left(F\right)\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to \underset{\dot{}}{1}\circ 1^{st}\left(F\right)\in \mathrm{V}$$
19	11 14 4 18	fvmptd	$$⊢\phi \to I\left(F\right)=\underset{\dot{}}{1}\circ 1^{st}\left(F\right)$$