MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sect Structured version   Visualization version   GIF version

Definition df-sect 16172
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
StepHypRef Expression
1 csect 16169 . 2 class Sect
2 vc . . 3 setvar 𝑐
3 ccat 16090 . . 3 class Cat
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
62cv 1473 . . . . 5 class 𝑐
7 cbs 15637 . . . . 5 class Base
86, 7cfv 5786 . . . 4 class (Base‘𝑐)
9 vf . . . . . . . . . 10 setvar 𝑓
109cv 1473 . . . . . . . . 9 class 𝑓
114cv 1473 . . . . . . . . . 10 class 𝑥
125cv 1473 . . . . . . . . . 10 class 𝑦
13 vh . . . . . . . . . . 11 setvar
1413cv 1473 . . . . . . . . . 10 class
1511, 12, 14co 6523 . . . . . . . . 9 class (𝑥𝑦)
1610, 15wcel 1975 . . . . . . . 8 wff 𝑓 ∈ (𝑥𝑦)
17 vg . . . . . . . . . 10 setvar 𝑔
1817cv 1473 . . . . . . . . 9 class 𝑔
1912, 11, 14co 6523 . . . . . . . . 9 class (𝑦𝑥)
2018, 19wcel 1975 . . . . . . . 8 wff 𝑔 ∈ (𝑦𝑥)
2116, 20wa 382 . . . . . . 7 wff (𝑓 ∈ (𝑥𝑦) ∧ 𝑔 ∈ (𝑦𝑥))
2211, 12cop 4126 . . . . . . . . . 10 class 𝑥, 𝑦
23 cco 15722 . . . . . . . . . . 11 class comp
246, 23cfv 5786 . . . . . . . . . 10 class (comp‘𝑐)
2522, 11, 24co 6523 . . . . . . . . 9 class (⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)
2618, 10, 25co 6523 . . . . . . . 8 class (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓)
27 ccid 16091 . . . . . . . . . 10 class Id
286, 27cfv 5786 . . . . . . . . 9 class (Id‘𝑐)
2911, 28cfv 5786 . . . . . . . 8 class ((Id‘𝑐)‘𝑥)
3026, 29wceq 1474 . . . . . . 7 wff (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥)
3121, 30wa 382 . . . . . 6 wff ((𝑓 ∈ (𝑥𝑦) ∧ 𝑔 ∈ (𝑦𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))
32 chom 15721 . . . . . . 7 class Hom
336, 32cfv 5786 . . . . . 6 class (Hom ‘𝑐)
3431, 13, 33wsbc 3397 . . . . 5 wff [(Hom ‘𝑐) / ]((𝑓 ∈ (𝑥𝑦) ∧ 𝑔 ∈ (𝑦𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))
3534, 9, 17copab 4632 . . . 4 class {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ]((𝑓 ∈ (𝑥𝑦) ∧ 𝑔 ∈ (𝑦𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}
364, 5, 8, 8, 35cmpt2 6525 . . 3 class (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ]((𝑓 ∈ (𝑥𝑦) ∧ 𝑔 ∈ (𝑦𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))})
372, 3, 36cmpt 4633 . 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ]((𝑓 ∈ (𝑥𝑦) ∧ 𝑔 ∈ (𝑦𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))
381, 37wceq 1474 1 wff Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ]((𝑓 ∈ (𝑥𝑦) ∧ 𝑔 ∈ (𝑦𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))
Colors of variables: wff setvar class
This definition is referenced by:  sectffval  16175
  Copyright terms: Public domain W3C validator