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 = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csect ⊢ Sect
1 vc ⊢ 𝑐
2 ccat ⊢ Cat
3 vx ⊢ 𝑥
4 cbs ⊢ Base
5 1 cv ⊢ 𝑐
6 5 4 cfv ⊢ ( Base ‘ 𝑐 )
7 vy ⊢ 𝑦
8 vf ⊢ 𝑓
9 vg ⊢ 𝑔
10 chom ⊢ Hom
11 5 10 cfv ⊢ ( Hom ‘ 𝑐 )
12 vh ⊢ ℎ
13 8 cv ⊢ 𝑓
14 3 cv ⊢ 𝑥
15 12 cv ⊢ ℎ
16 7 cv ⊢ 𝑦
17 14 16 15 co ⊢ ( 𝑥 ℎ 𝑦 )
18 13 17 wcel ⊢ 𝑓 ∈ ( 𝑥 ℎ 𝑦 )
19 9 cv ⊢ 𝑔
20 16 14 15 co ⊢ ( 𝑦 ℎ 𝑥 )
21 19 20 wcel ⊢ 𝑔 ∈ ( 𝑦 ℎ 𝑥 )
22 18 21 wa ⊢ ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) )
23 14 16 cop ⊢ ⟨ 𝑥 , 𝑦 ⟩
24 cco ⊢ comp
25 5 24 cfv ⊢ ( comp ‘ 𝑐 )
26 23 14 25 co ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 )
27 19 13 26 co ⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 )
28 ccid ⊢ Id
29 5 28 cfv ⊢ ( Id ‘ 𝑐 )
30 14 29 cfv ⊢ ( ( Id ‘ 𝑐 ) ‘ 𝑥 )
31 27 30 wceq ⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 )
32 22 31 wa ⊢ ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) )
33 32 12 11 wsbc ⊢ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) )
34 33 8 9 copab ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) }
35 3 7 6 6 34 cmpo ⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } )
36 1 2 35 cmpt ⊢ ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } ) )
37 0 36 wceq ⊢ Sect = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } ) )