Metamath Proof Explorer

Definition df-sect

Description: Function returning the section relation in a category. Given arrows f : X --> Y and g : Y --> X , we say f Sect g , that is, f is a section of g , if g o. f = 1X . If there there is an arrow g with f Sect g , the arrow f is called a section, see definition 7.19 of Adamek p. 106. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-sect ⊢ Sect = c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ f g | [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 csect class Sect
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 vf setvar f
9 vg setvar g
10 chom class Hom
11 5 10 cfv class Hom ⁡ c
12 vh setvar h
13 8 cv setvar f
14 3 cv setvar x
15 12 cv setvar h
16 7 cv setvar y
17 14 16 15 co class x h y
18 13 17 wcel wff f ∈ x h y
19 9 cv setvar g
20 16 14 15 co class y h x
21 19 20 wcel wff g ∈ y h x
22 18 21 wa wff f ∈ x h y ∧ g ∈ y h x
23 14 16 cop class x y
24 cco class comp
25 5 24 cfv class comp ⁡ c
26 23 14 25 co class x y comp ⁡ c x
27 19 13 26 co class g x y comp ⁡ c x f
28 ccid class Id
29 5 28 cfv class Id ⁡ c
30 14 29 cfv class Id ⁡ c ⁡ x
31 27 30 wceq wff g x y comp ⁡ c x f = Id ⁡ c ⁡ x
32 22 31 wa wff f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x
33 32 12 11 wsbc wff [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x
34 33 8 9 copab class f g | [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x
35 3 7 6 6 34 cmpo class x ∈ Base c , y ∈ Base c ⟼ f g | [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x
36 1 2 35 cmpt class c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ f g | [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x
37 0 36 wceq wff Sect = c ∈ Cat ⟼ x ∈ Base c , y ∈ Base c ⟼ f g | [˙ Hom ⁡ c / h]˙ f ∈ x h y ∧ g ∈ y h x ∧ g x y comp ⁡ c x f = Id ⁡ c ⁡ x