Metamath Proof Explorer


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 Cat x V dom x Inv c

Detailed syntax breakdown

Step Hyp Ref Expression
0 ciso class Iso
1 vc setvar c
2 ccat class Cat
3 vx setvar x
4 cvv class V
5 3 cv setvar x
6 5 cdm class dom x
7 3 4 6 cmpt class x V dom x
8 cinv class Inv
9 1 cv setvar c
10 9 8 cfv class Inv c
11 7 10 ccom class x V dom x Inv c
12 1 2 11 cmpt class c Cat x V dom x Inv c
13 0 12 wceq wff Iso = c Cat x V dom x Inv c