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