Definition df-iso 17013

Description: Function returning the isomorphisms of the category 𝑐. 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 = (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐)))

Distinct variable group:   𝑥,𝑐

Detailed syntax breakdown of Definition df-iso

Step	Hyp	Ref	Expression
1		ciso 17010	. 2 class Iso
2		vc	. . 3 setvar 𝑐
3		ccat 16929	. . 3 class Cat
4		vx	. . . . 5 setvar 𝑥
5		cvv 3495	. . . . 5 class V
6	4	cv 1532	. . . . . 6 class 𝑥
7	6	cdm 5550	. . . . 5 class dom 𝑥
8	4, 5, 7	cmpt 5139	. . . 4 class (𝑥 ∈ V ↦ dom 𝑥)
9	2	cv 1532	. . . . 5 class 𝑐
10		cinv 17009	. . . . 5 class Inv
11	9, 10	cfv 6350	. . . 4 class (Inv‘𝑐)
12	8, 11	ccom 5554	. . 3 class ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐))
13	2, 3, 12	cmpt 5139	. 2 class (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐)))
14	1, 13	wceq 1533	1 wff Iso = (𝑐 ∈ Cat ↦ ((𝑥 ∈ V ↦ dom 𝑥) ∘ (Inv‘𝑐)))

This definition is referenced by:  isofval  17021