Metamath Proof Explorer

Theorem sectffval

Description: Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017) Removed redundant hypotheses. (Revised by Zhi Wang, 27-Oct-2025)

Ref Expression
Hypotheses issect.b 
|- B = ( Base ` C )
issect.h 
|- H = ( Hom ` C )
issect.o 
|- .x. = ( comp ` C )
issect.i 
|- .1. = ( Id ` C )
issect.s 
|- S = ( Sect ` C )
issect.c 
|- ( ph -> C e. Cat )
Assertion sectffval 
|- ( ph -> S = ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) } ) )

Proof

Step Hyp Ref Expression
1 issect.b 
 |-  B = ( Base ` C )
2 issect.h 
 |-  H = ( Hom ` C )
3 issect.o 
 |-  .x. = ( comp ` C )
4 issect.i 
 |-  .1. = ( Id ` C )
5 issect.s 
 |-  S = ( Sect ` C )
6 issect.c 
 |-  ( ph -> C e. Cat )
7 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
8 7 1 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
9 fvexd 
 |-  ( c = C -> ( Hom ` c ) e. _V )
10 fveq2 
 |-  ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
11 10 2 eqtr4di 
 |-  ( c = C -> ( Hom ` c ) = H )
12 simpr 
 |-  ( ( c = C /\ h = H ) -> h = H )
13 12 oveqd 
 |-  ( ( c = C /\ h = H ) -> ( x h y ) = ( x H y ) )
14 13 eleq2d 
 |-  ( ( c = C /\ h = H ) -> ( f e. ( x h y ) <-> f e. ( x H y ) ) )
15 12 oveqd 
 |-  ( ( c = C /\ h = H ) -> ( y h x ) = ( y H x ) )
16 15 eleq2d 
 |-  ( ( c = C /\ h = H ) -> ( g e. ( y h x ) <-> g e. ( y H x ) ) )
17 14 16 anbi12d 
 |-  ( ( c = C /\ h = H ) -> ( ( f e. ( x h y ) /\ g e. ( y h x ) ) <-> ( f e. ( x H y ) /\ g e. ( y H x ) ) ) )
18 simpl 
 |-  ( ( c = C /\ h = H ) -> c = C )
19 18 fveq2d 
 |-  ( ( c = C /\ h = H ) -> ( comp ` c ) = ( comp ` C ) )
20 19 3 eqtr4di 
 |-  ( ( c = C /\ h = H ) -> ( comp ` c ) = .x. )
21 20 oveqd 
 |-  ( ( c = C /\ h = H ) -> ( <. x , y >. ( comp ` c ) x ) = ( <. x , y >. .x. x ) )
22 21 oveqd 
 |-  ( ( c = C /\ h = H ) -> ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( g ( <. x , y >. .x. x ) f ) )
23 18 fveq2d 
 |-  ( ( c = C /\ h = H ) -> ( Id ` c ) = ( Id ` C ) )
24 23 4 eqtr4di 
 |-  ( ( c = C /\ h = H ) -> ( Id ` c ) = .1. )
25 24 fveq1d 
 |-  ( ( c = C /\ h = H ) -> ( ( Id ` c ) ` x ) = ( .1. ` x ) )
26 22 25 eqeq12d 
 |-  ( ( c = C /\ h = H ) -> ( ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) <-> ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) )
27 17 26 anbi12d 
 |-  ( ( c = C /\ h = H ) -> ( ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) <-> ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) ) )
28 9 11 27 sbcied2 
 |-  ( c = C -> ( [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) <-> ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) ) )
29 28 opabbidv 
 |-  ( c = C -> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } = { <. f , g >. | ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) } )
30 8 8 29 mpoeq123dv 
 |-  ( c = C -> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) = ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) } ) )
31 df-sect 
 |-  Sect = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )
32 1 fvexi 
 |-  B e. _V
33 32 32 mpoex 
 |-  ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) } ) e. _V
34 30 31 33 fvmpt 
 |-  ( C e. Cat -> ( Sect ` C ) = ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) } ) )
35 6 34 syl 
 |-  ( ph -> ( Sect ` C ) = ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) } ) )
36 5 35 eqtrid 
 |-  ( ph -> S = ( x e. B , y e. B |-> { <. f , g >. | ( ( f e. ( x H y ) /\ g e. ( y H x ) ) /\ ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) } ) )