This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem invffval

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

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