Definition df-iso

Description: Function returning the isomorphisms of the category c . Definition 3.8 of Adamek p. 28, and definition in Lang p. 54. (Contributed by FL, 9-Jun-2014) (Revised by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	df-iso	|- Iso = ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. ( Inv ` c ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciso	|- Iso
1		vc	|- c
2		ccat	|- Cat
3		vx	|- x
4		cvv	|- _V
5	3	cv	|- x
6	5	cdm	|- dom x
7	3 4 6	cmpt	|- ( x e. _V |-> dom x )
8		cinv	|- Inv
9	1	cv	|- c
10	9 8	cfv	|- ( Inv ` c )
11	7 10	ccom	|- ( ( x e. _V |-> dom x ) o. ( Inv ` c ) )
12	1 2 11	cmpt	|- ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. ( Inv ` c ) ) )
13	0 12	wceq	|- Iso = ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. ( Inv ` c ) ) )