Definition df-iso 16409

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

Assertion

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

Distinct variable group:   x, c

Detailed syntax breakdown of Definition df-iso

Step	Hyp	Ref	Expression
1		ciso 16406	. 2 class Iso
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4		vx	. . . . 5 setvar x
5		cvv 3200	. . . . 5 class _V
6	4	cv 1482	. . . . . 6 class x
7	6	cdm 5114	. . . . 5 class dom x
8	4, 5, 7	cmpt 4729	. . . 4 class ( x e. _V |-> dom x )
9	2	cv 1482	. . . . 5 class c
10		cinv 16405	. . . . 5 class Inv
11	9, 10	cfv 5888	. . . 4 class (Inv ` c )
12	8, 11	ccom 5118	. . 3 class ( ( x e. _V |-> dom x ) o. (Inv ` c ) )
13	2, 3, 12	cmpt 4729	. 2 class ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. (Inv ` c ) ) )
14	1, 13	wceq 1483	1 wff Iso = ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. (Inv ` c ) ) )

This definition is referenced by:  isofval  16417