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 = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cinv	⊢ Inv
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑐
6	5 4	cfv	⊢ ( Base ‘ 𝑐 )
7		vy	⊢ 𝑦
8	3	cv	⊢ 𝑥
9		csect	⊢ Sect
10	5 9	cfv	⊢ ( Sect ‘ 𝑐 )
11	7	cv	⊢ 𝑦
12	8 11 10	co	⊢ ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 )
13	11 8 10	co	⊢ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 )
14	13	ccnv	⊢ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 )
15	12 14	cin	⊢ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) )
16	3 7 6 6 15	cmpo	⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) )
17	1 2 16	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) )
18	0 17	wceq	⊢ Inv = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) )