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 e. Cat -> ( Sect ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } )
2 ovex 
 |-  ( x ( Hom ` C ) y ) e. _V
3 ovex 
 |-  ( y ( Hom ` C ) x ) e. _V
4 2 3 xpex 
 |-  ( ( x ( Hom ` C ) y ) X. ( y ( Hom ` C ) x ) ) e. _V
5 opabssxp 
 |-  { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } C_ ( ( x ( Hom ` C ) y ) X. ( y ( Hom ` C ) x ) )
6 4 5 ssexi 
 |-  { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } e. _V
7 1 6 fnmpoi 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) Fn ( ( Base ` C ) X. ( 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 e. Cat -> C e. Cat )
14 8 9 10 11 12 13 sectffval 
 |-  ( C e. Cat -> ( Sect ` C ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) )
15 14 fneq1d 
 |-  ( C e. Cat -> ( ( Sect ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) )
16 7 15 mpbiri 
 |-  ( C e. Cat -> ( Sect ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )