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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catccatid.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	catcid.o	⊢ 1 = ( Id ‘ 𝐶 )
	catcid.i	⊢ 𝐼 = ( idfunc ‘ 𝑋 )
	catcid.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	catcid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	catcid	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		catccatid.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catccatid.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		catcid.o	⊢ 1 = ( Id ‘ 𝐶 )
4		catcid.i	⊢ 𝐼 = ( idfunc ‘ 𝑋 )
5		catcid.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6		catcid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7	1 2	catccatid	⊢ ( 𝑈 ∈ 𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ ( idfunc ‘ 𝑥 ) ) ) )
8	5 7	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ ( idfunc ‘ 𝑥 ) ) ) )
9	8	simprd	⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ ( idfunc ‘ 𝑥 ) ) )
10	3 9	syl5eq	⊢ ( 𝜑 → 1 = ( 𝑥 ∈ 𝐵 ↦ ( idfunc ‘ 𝑥 ) ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( idfunc ‘ 𝑥 ) = ( idfunc ‘ 𝑋 ) )
13		fvexd	⊢ ( 𝜑 → ( idfunc ‘ 𝑋 ) ∈ V )
14	10 12 6 13	fvmptd	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( idfunc ‘ 𝑋 ) )
15	14 4	eqtr4di	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = 𝐼 )