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 ) ) ) )