Theorem idafval

Description: Value of the identity arrow function. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	idafval.i	⊢ 𝐼 = ( Ida ‘ 𝐶 )
	idafval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	idafval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	idafval.1	⊢ 1 = ( Id ‘ 𝐶 )
Assertion	idafval	⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ ⟨ 𝑥 , 𝑥 , ( 1 ‘ 𝑥 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		idafval.i	⊢ 𝐼 = ( Ida ‘ 𝐶 )
2		idafval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		idafval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		idafval.1	⊢ 1 = ( Id ‘ 𝐶 )
5		fveq2	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
6	5 2	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
7		fveq2	⊢ ( 𝑐 = 𝐶 → ( Id ‘ 𝑐 ) = ( Id ‘ 𝐶 ) )
8	7 4	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Id ‘ 𝑐 ) = 1 )
9	8	fveq1d	⊢ ( 𝑐 = 𝐶 → ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) = ( 1 ‘ 𝑥 ) )
10	9	oteq3d	⊢ ( 𝑐 = 𝐶 → ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ⟩ = ⟨ 𝑥 , 𝑥 , ( 1 ‘ 𝑥 ) ⟩ )
11	6 10	mpteq12dv	⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ 𝐵 ↦ ⟨ 𝑥 , 𝑥 , ( 1 ‘ 𝑥 ) ⟩ ) )
12		df-ida	⊢ Ida = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ⟩ ) )
13	11 12 2	mptfvmpt	⊢ ( 𝐶 ∈ Cat → ( Ida ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ ⟨ 𝑥 , 𝑥 , ( 1 ‘ 𝑥 ) ⟩ ) )
14	3 13	syl	⊢ ( 𝜑 → ( Ida ‘ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ ⟨ 𝑥 , 𝑥 , ( 1 ‘ 𝑥 ) ⟩ ) )
15	1 14	syl5eq	⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ ⟨ 𝑥 , 𝑥 , ( 1 ‘ 𝑥 ) ⟩ ) )