Theorem fucid

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

	Ref	Expression
Hypotheses	fucid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucid.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
	fucid.1	⊢ 1 = ( Id ‘ 𝐷 )
	fucid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	fucid	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐹 ) = ( 1 ∘ ( 1st ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		fucid.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
3		fucid.1	⊢ 1 = ( Id ‘ 𝐷 )
4		fucid.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
6	4 5	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
7	6	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
8	6	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
9	1 7 8 3	fuccatid	⊢ ( 𝜑 → ( 𝑄 ∈ Cat ∧ ( Id ‘ 𝑄 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1 ∘ ( 1st ‘ 𝑓 ) ) ) ) )
10	9	simprd	⊢ ( 𝜑 → ( Id ‘ 𝑄 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1 ∘ ( 1st ‘ 𝑓 ) ) ) )
11	2 10	syl5eq	⊢ ( 𝜑 → 𝐼 = ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ↦ ( 1 ∘ ( 1st ‘ 𝑓 ) ) ) )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
13	12	fveq2d	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 1st ‘ 𝑓 ) = ( 1st ‘ 𝐹 ) )
14	13	coeq2d	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ( 1 ∘ ( 1st ‘ 𝑓 ) ) = ( 1 ∘ ( 1st ‘ 𝐹 ) ) )
15	3	fvexi	⊢ 1 ∈ V
16		fvex	⊢ ( 1st ‘ 𝐹 ) ∈ V
17	15 16	coex	⊢ ( 1 ∘ ( 1st ‘ 𝐹 ) ) ∈ V
18	17	a1i	⊢ ( 𝜑 → ( 1 ∘ ( 1st ‘ 𝐹 ) ) ∈ V )
19	11 14 4 18	fvmptd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝐹 ) = ( 1 ∘ ( 1st ‘ 𝐹 ) ) )