This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC CATEGORY THEORY Categories Sections, inverses, isomorphisms 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 ‘ 𝑐 ) 𝑥 ) ) ) )