Metamath Proof Explorer

Definition df-inv

Description: The inverse relation in a category. Given arrows f : X --> Y and g : Y --> X , we say g Inv f , that is, g is an inverse of f , if g is a section of f and f is a section of g . Definition 3.8 of Adamek p. 28. (Contributed by FL, 22-Dec-2008) (Revised by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-inv ⊢ Inv = c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ x Sect ⁡ c y ∩ y Sect ⁡ c x -1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinv class Inv
1 vc setvar c
2 ccat class Cat
3 vx setvar x
4 cbs class Base
5 1 cv setvar c
6 5 4 cfv class Base c
7 vy setvar y
8 3 cv setvar x
9 csect class Sect
10 5 9 cfv class Sect ⁡ c
11 7 cv setvar y
12 8 11 10 co class x Sect ⁡ c y
13 11 8 10 co class y Sect ⁡ c x
14 13 ccnv class y Sect ⁡ c x -1
15 12 14 cin class x Sect ⁡ c y ∩ y Sect ⁡ c x -1
16 3 7 6 6 15 cmpo class x ∈ Base c , y ∈ Base c ⟼ x Sect ⁡ c y ∩ y Sect ⁡ c x -1
17 1 2 16 cmpt class c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ x Sect ⁡ c y ∩ y Sect ⁡ c x -1
18 0 17 wceq wff Inv = c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ x Sect ⁡ c y ∩ y Sect ⁡ c x -1