# 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 ${⊢}\mathrm{Iso}=\left({c}\in \mathrm{Cat}⟼\left({x}\in \mathrm{V}⟼\mathrm{dom}{x}\right)\circ \mathrm{Inv}\left({c}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ciso ${class}\mathrm{Iso}$
1 vc ${setvar}{c}$
2 ccat ${class}\mathrm{Cat}$
3 vx ${setvar}{x}$
4 cvv ${class}\mathrm{V}$
5 3 cv ${setvar}{x}$
6 5 cdm ${class}\mathrm{dom}{x}$
7 3 4 6 cmpt ${class}\left({x}\in \mathrm{V}⟼\mathrm{dom}{x}\right)$
8 cinv ${class}\mathrm{Inv}$
9 1 cv ${setvar}{c}$
10 9 8 cfv ${class}\mathrm{Inv}\left({c}\right)$
11 7 10 ccom ${class}\left(\left({x}\in \mathrm{V}⟼\mathrm{dom}{x}\right)\circ \mathrm{Inv}\left({c}\right)\right)$
12 1 2 11 cmpt ${class}\left({c}\in \mathrm{Cat}⟼\left({x}\in \mathrm{V}⟼\mathrm{dom}{x}\right)\circ \mathrm{Inv}\left({c}\right)\right)$
13 0 12 wceq ${wff}\mathrm{Iso}=\left({c}\in \mathrm{Cat}⟼\left({x}\in \mathrm{V}⟼\mathrm{dom}{x}\right)\circ \mathrm{Inv}\left({c}\right)\right)$