Definition df-sect 17459

Description: Function returning the section relation in a category. Given arrows 𝑓:𝑋⟶𝑌 and 𝑔:𝑌⟶𝑋, we say 𝑓Sect𝑔, that is, 𝑓 is a section of 𝑔, if 𝑔 ∘ 𝑓 = 1‘𝑋. If there there is an arrow 𝑔 with 𝑓Sect𝑔, the arrow 𝑓 is called a section, see definition 7.19 of [Adamek] p. 106. (Contributed by Mario Carneiro, 2-Jan-2017.)

Assertion

Ref	Expression
df-sect	⊢ Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))

Distinct variable group:   𝑓,𝑐,𝑔,ℎ,𝑥,𝑦

Detailed syntax breakdown of Definition df-sect

Step	Hyp	Ref	Expression
1		csect 17456	. 2 class Sect
2		vc	. . 3 setvar 𝑐
3		ccat 17373	. . 3 class Cat
4		vx	. . . 4 setvar 𝑥
5		vy	. . . 4 setvar 𝑦
6	2	cv 1538	. . . . 5 class 𝑐
7		cbs 16912	. . . . 5 class Base
8	6, 7	cfv 6433	. . . 4 class (Base‘𝑐)
9		vf	. . . . . . . . . 10 setvar 𝑓
10	9	cv 1538	. . . . . . . . 9 class 𝑓
11	4	cv 1538	. . . . . . . . . 10 class 𝑥
12	5	cv 1538	. . . . . . . . . 10 class 𝑦
13		vh	. . . . . . . . . . 11 setvar ℎ
14	13	cv 1538	. . . . . . . . . 10 class ℎ
15	11, 12, 14	co 7275	. . . . . . . . 9 class (𝑥ℎ𝑦)
16	10, 15	wcel 2106	. . . . . . . 8 wff 𝑓 ∈ (𝑥ℎ𝑦)
17		vg	. . . . . . . . . 10 setvar 𝑔
18	17	cv 1538	. . . . . . . . 9 class 𝑔
19	12, 11, 14	co 7275	. . . . . . . . 9 class (𝑦ℎ𝑥)
20	18, 19	wcel 2106	. . . . . . . 8 wff 𝑔 ∈ (𝑦ℎ𝑥)
21	16, 20	wa 396	. . . . . . 7 wff (𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥))
22	11, 12	cop 4567	. . . . . . . . . 10 class ⟨𝑥, 𝑦⟩
23		cco 16974	. . . . . . . . . . 11 class comp
24	6, 23	cfv 6433	. . . . . . . . . 10 class (comp‘𝑐)
25	22, 11, 24	co 7275	. . . . . . . . 9 class (⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)
26	18, 10, 25	co 7275	. . . . . . . 8 class (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓)
27		ccid 17374	. . . . . . . . . 10 class Id
28	6, 27	cfv 6433	. . . . . . . . 9 class (Id‘𝑐)
29	11, 28	cfv 6433	. . . . . . . 8 class ((Id‘𝑐)‘𝑥)
30	26, 29	wceq 1539	. . . . . . 7 wff (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥)
31	21, 30	wa 396	. . . . . 6 wff ((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))
32		chom 16973	. . . . . . 7 class Hom
33	6, 32	cfv 6433	. . . . . 6 class (Hom ‘𝑐)
34	31, 13, 33	wsbc 3716	. . . . 5 wff [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))
35	34, 9, 17	copab 5136	. . . 4 class {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}
36	4, 5, 8, 8, 35	cmpo 7277	. . 3 class (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))})
37	2, 3, 36	cmpt 5157	. 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))
38	1, 37	wceq 1539	1 wff Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))

This definition is referenced by:  sectffval  17462