Definition df-ida 18005

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.)

Assertion

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

Distinct variable group:   𝑥,𝑐

Detailed syntax breakdown of Definition df-ida

Step	Hyp	Ref	Expression
1		cida 18003	. 2 class Ida
2		vc	. . 3 setvar 𝑐
3		ccat 17608	. . 3 class Cat
4		vx	. . . 4 setvar 𝑥
5	2	cv 1541	. . . . 5 class 𝑐
6		cbs 17144	. . . . 5 class Base
7	5, 6	cfv 6544	. . . 4 class (Base‘𝑐)
8	4	cv 1541	. . . . 5 class 𝑥
9		ccid 17609	. . . . . . 7 class Id
10	5, 9	cfv 6544	. . . . . 6 class (Id‘𝑐)
11	8, 10	cfv 6544	. . . . 5 class ((Id‘𝑐)‘𝑥)
12	8, 8, 11	cotp 4637	. . . 4 class ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩
13	4, 7, 12	cmpt 5232	. . 3 class (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩)
14	2, 3, 13	cmpt 5232	. 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))
15	1, 14	wceq 1542	1 wff Ida = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ ⟨𝑥, 𝑥, ((Id‘𝑐)‘𝑥)⟩))

This definition is referenced by:  idafval  18007