Metamath Proof Explorer

Theorem sectffval

Description: Value of the section operation. (Contributed by Mario Carneiro, 2-Jan-2017)

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 )
issect.x 
|- ( ph -> X e. B )
issect.y 
|- ( ph -> Y e. B )
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 issect.x 
 |-  ( ph -> X e. B )
8 issect.y 
 |-  ( ph -> Y e. B )
9 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
10 9 1 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
11 fvexd 
 |-  ( c = C -> ( Hom ` c ) e. _V )
12 fveq2 
 |-  ( c = C -> ( Hom ` c ) = ( Hom ` C ) )
13 12 2 eqtr4di 
 |-  ( c = C -> ( Hom ` c ) = H )
14 simpr 
 |-  ( ( c = C /\ h = H ) -> h = H )
15 14 oveqd 
 |-  ( ( c = C /\ h = H ) -> ( x h y ) = ( x H y ) )
16 15 eleq2d 
 |-  ( ( c = C /\ h = H ) -> ( f e. ( x h y ) <-> f e. ( x H y ) ) )
17 14 oveqd 
 |-  ( ( c = C /\ h = H ) -> ( y h x ) = ( y H x ) )
18 17 eleq2d 
 |-  ( ( c = C /\ h = H ) -> ( g e. ( y h x ) <-> g e. ( y H x ) ) )
19 16 18 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 ) ) ) )
20 simpl 
 |-  ( ( c = C /\ h = H ) -> c = C )
21 20 fveq2d 
 |-  ( ( c = C /\ h = H ) -> ( comp ` c ) = ( comp ` C ) )
22 21 3 eqtr4di 
 |-  ( ( c = C /\ h = H ) -> ( comp ` c ) = .x. )
23 22 oveqd 
 |-  ( ( c = C /\ h = H ) -> ( <. x , y >. ( comp ` c ) x ) = ( <. x , y >. .x. x ) )
24 23 oveqd 
 |-  ( ( c = C /\ h = H ) -> ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( g ( <. x , y >. .x. x ) f ) )
25 20 fveq2d 
 |-  ( ( c = C /\ h = H ) -> ( Id ` c ) = ( Id ` C ) )
26 25 4 eqtr4di 
 |-  ( ( c = C /\ h = H ) -> ( Id ` c ) = .1. )
27 26 fveq1d 
 |-  ( ( c = C /\ h = H ) -> ( ( Id ` c ) ` x ) = ( .1. ` x ) )
28 24 27 eqeq12d 
 |-  ( ( c = C /\ h = H ) -> ( ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) <-> ( g ( <. x , y >. .x. x ) f ) = ( .1. ` x ) ) )
29 19 28 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 ) ) ) )
30 11 13 29 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 ) ) ) )
31 30 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 ) ) } )
32 10 10 31 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 ) ) } ) )
33 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 ) ) } ) )
34 1 fvexi 
 |-  B e. _V
35 34 34 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
36 32 33 35 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 ) ) } ) )
37 6 36 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 ) ) } ) )
38 5 37 syl5eq 
 |-  ( 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 ) ) } ) )