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	$$⊢\mathrm{Inv}=\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(x\mathrm{Sect}\left(c\right)y\right)\cap {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinv	$$class\mathrm{Inv}$$
1		vc	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarc$$
6	5 4	cfv	$$class{\mathrm{Base}}_c$$
7		vy	$$setvary$$
8	3	cv	$$setvarx$$
9		csect	$$class\mathrm{Sect}$$
10	5 9	cfv	$$class\mathrm{Sect}\left(c\right)$$
11	7	cv	$$setvary$$
12	8 11 10	co	$$class\left(x\mathrm{Sect}\left(c\right)y\right)$$
13	11 8 10	co	$$class\left(y\mathrm{Sect}\left(c\right)x\right)$$
14	13	ccnv	$$class{\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}$$
15	12 14	cin	$$class\left(\left(x\mathrm{Sect}\left(c\right)y\right)\cap {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}\right)$$
16	3 7 6 6 15	cmpo	$$class\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(x\mathrm{Sect}\left(c\right)y\right)\cap {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}\right)$$
17	1 2 16	cmpt	$$class\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(x\mathrm{Sect}\left(c\right)y\right)\cap {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}\right)\right)$$
18	0 17	wceq	$$wff\mathrm{Inv}=\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(x\mathrm{Sect}\left(c\right)y\right)\cap {\left(y\mathrm{Sect}\left(c\right)x\right)}^{-1}\right)\right)$$