Definition df-ida

Description: Definition of the identity arrow, which is just the identity morphism tagged with its domain and codomain. (Contributed by FL, 26-Oct-2007) (Revised by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Assertion	df-ida	⊢ Ida = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cida	⊢ Ida
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑐
6	5 4	cfv	⊢ ( Base ‘ 𝑐 )
7	3	cv	⊢ 𝑥
8		ccid	⊢ Id
9	5 8	cfv	⊢ ( Id ‘ 𝑐 )
10	7 9	cfv	⊢ ( ( Id ‘ 𝑐 ) ‘ 𝑥 )
11	7 7 10	cotp	⊢ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ⟩
12	3 6 11	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ⟩ )
13	1 2 12	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ⟩ ) )
14	0 13	wceq	⊢ Ida = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ⟨ 𝑥 , 𝑥 , ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ⟩ ) )