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	$$⊢{Id}_a=\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c⟼⟨x,x,\mathrm{Id}\left(c\right)\left(x\right)⟩\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cida	$$class{Id}_a$$
1		vc	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarc$$
6	5 4	cfv	$$class{\mathrm{Base}}_c$$
7	3	cv	$$setvarx$$
8		ccid	$$class\mathrm{Id}$$
9	5 8	cfv	$$class\mathrm{Id}\left(c\right)$$
10	7 9	cfv	$$class\mathrm{Id}\left(c\right)\left(x\right)$$
11	7 7 10	cotp	$$class⟨x,x,\mathrm{Id}\left(c\right)\left(x\right)⟩$$
12	3 6 11	cmpt	$$class\left(x\in {\mathrm{Base}}_c⟼⟨x,x,\mathrm{Id}\left(c\right)\left(x\right)⟩\right)$$
13	1 2 12	cmpt	$$class\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c⟼⟨x,x,\mathrm{Id}\left(c\right)\left(x\right)⟩\right)\right)$$
14	0 13	wceq	$$wff{Id}_a=\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c⟼⟨x,x,\mathrm{Id}\left(c\right)\left(x\right)⟩\right)\right)$$