Metamath Proof Explorer

Theorem invffval

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

Ref Expression
Hypotheses invfval.b 
|- B = ( Base ` C )
invfval.n 
|- N = ( Inv ` C )
invfval.c 
|- ( ph -> C e. Cat )
invfval.x 
|- ( ph -> X e. B )
invfval.y 
|- ( ph -> Y e. B )
invfval.s 
|- S = ( Sect ` C )
Assertion invffval 
|- ( ph -> N = ( x e. B , y e. B |-> ( ( x S y ) i^i `' ( y S x ) ) ) )

Proof

Step Hyp Ref Expression
1 invfval.b 
 |-  B = ( Base ` C )
2 invfval.n 
 |-  N = ( Inv ` C )
3 invfval.c 
 |-  ( ph -> C e. Cat )
4 invfval.x 
 |-  ( ph -> X e. B )
5 invfval.y 
 |-  ( ph -> Y e. B )
6 invfval.s 
 |-  S = ( Sect ` C )
7 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
8 7 1 eqtr4di 
 |-  ( c = C -> ( Base ` c ) = B )
9 fveq2 
 |-  ( c = C -> ( Sect ` c ) = ( Sect ` C ) )
10 9 6 eqtr4di 
 |-  ( c = C -> ( Sect ` c ) = S )
11 10 oveqd 
 |-  ( c = C -> ( x ( Sect ` c ) y ) = ( x S y ) )
12 10 oveqd 
 |-  ( c = C -> ( y ( Sect ` c ) x ) = ( y S x ) )
13 12 cnveqd 
 |-  ( c = C -> `' ( y ( Sect ` c ) x ) = `' ( y S x ) )
14 11 13 ineq12d 
 |-  ( c = C -> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) = ( ( x S y ) i^i `' ( y S x ) ) )
15 8 8 14 mpoeq123dv 
 |-  ( c = C -> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) ) = ( x e. B , y e. B |-> ( ( x S y ) i^i `' ( y S x ) ) ) )
16 df-inv 
 |-  Inv = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) ) )
17 1 fvexi 
 |-  B e. _V
18 17 17 mpoex 
 |-  ( x e. B , y e. B |-> ( ( x S y ) i^i `' ( y S x ) ) ) e. _V
19 15 16 18 fvmpt 
 |-  ( C e. Cat -> ( Inv ` C ) = ( x e. B , y e. B |-> ( ( x S y ) i^i `' ( y S x ) ) ) )
20 3 19 syl 
 |-  ( ph -> ( Inv ` C ) = ( x e. B , y e. B |-> ( ( x S y ) i^i `' ( y S x ) ) ) )
21 2 20 eqtrid 
 |-  ( ph -> N = ( x e. B , y e. B |-> ( ( x S y ) i^i `' ( y S x ) ) ) )