Metamath Proof Explorer

Theorem sectfn

Description: The function value of the function returning the sections of a category is a function over the Cartesian square of the base set of the category. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion sectfn ⊢ C ∈ Cat → Sect ⁡ C Fn Base C × Base C

Proof

Step Hyp Ref Expression
1 eqid ⊢ x ∈ Base C , y ∈ Base C ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x = x ∈ Base C , y ∈ Base C ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x
2 ovex ⊢ x Hom ⁡ C y ∈ V
3 ovex ⊢ y Hom ⁡ C x ∈ V
4 2 3 xpex ⊢ x Hom ⁡ C y × y Hom ⁡ C x ∈ V
5 opabssxp ⊢ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x ⊆ x Hom ⁡ C y × y Hom ⁡ C x
6 4 5 ssexi ⊢ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x ∈ V
7 1 6 fnmpoi ⊢ x ∈ Base C , y ∈ Base C ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x Fn Base C × Base C
8 eqid ⊢ Base C = Base C
9 eqid ⊢ Hom ⁡ C = Hom ⁡ C
10 eqid ⊢ comp ⁡ C = comp ⁡ C
11 eqid ⊢ Id ⁡ C = Id ⁡ C
12 eqid ⊢ Sect ⁡ C = Sect ⁡ C
13 id ⊢ C ∈ Cat → C ∈ Cat
14 8 9 10 11 12 13 sectffval ⊢ C ∈ Cat → Sect ⁡ C = x ∈ Base C , y ∈ Base C ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x
15 14 fneq1d ⊢ C ∈ Cat → Sect ⁡ C Fn Base C × Base C ↔ x ∈ Base C , y ∈ Base C ⟼ f g | f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C x ∧ g x y comp ⁡ C x f = Id ⁡ C ⁡ x Fn Base C × Base C
16 7 15 mpbiri ⊢ C ∈ Cat → Sect ⁡ C Fn Base C × Base C