Metamath Proof Explorer

Theorem invfn

Description: The function value of the function returning the inverses of a category is a function over the Cartesian square of the base set of the category. Simplifies isofn (see isofnALT ). (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion invfn 
|- ( C e. Cat -> ( Inv ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )

Proof

Step Hyp Ref Expression
1 ovex 
 |-  ( x ( Sect ` C ) y ) e. _V
2 1 inex1 
 |-  ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) e. _V
3 2 a1i 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) e. _V )
4 3 ralrimivva 
 |-  ( C e. Cat -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) e. _V )
5 eqid 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) )
6 5 fnmpo 
 |-  ( A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) e. _V -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
7 4 6 syl 
 |-  ( C e. Cat -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
8 df-inv 
 |-  Inv = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) ) )
9 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
10 fveq2 
 |-  ( c = C -> ( Sect ` c ) = ( Sect ` C ) )
11 10 oveqd 
 |-  ( c = C -> ( x ( Sect ` c ) y ) = ( x ( Sect ` C ) y ) )
12 10 oveqd 
 |-  ( c = C -> ( y ( Sect ` c ) x ) = ( y ( Sect ` C ) x ) )
13 12 cnveqd 
 |-  ( c = C -> `' ( y ( Sect ` c ) x ) = `' ( y ( Sect ` C ) x ) )
14 11 13 ineq12d 
 |-  ( c = C -> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) = ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) )
15 9 9 14 mpoeq123dv 
 |-  ( c = C -> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) )
16 id 
 |-  ( C e. Cat -> C e. Cat )
17 fvex 
 |-  ( Base ` C ) e. _V
18 17 17 pm3.2i 
 |-  ( ( Base ` C ) e. _V /\ ( Base ` C ) e. _V )
19 mpoexga 
 |-  ( ( ( Base ` C ) e. _V /\ ( Base ` C ) e. _V ) -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) e. _V )
20 18 19 mp1i 
 |-  ( C e. Cat -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) e. _V )
21 8 15 16 20 fvmptd3 
 |-  ( C e. Cat -> ( Inv ` C ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) )
22 21 fneq1d 
 |-  ( C e. Cat -> ( ( Inv ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) )
23 7 22 mpbird 
 |-  ( C e. Cat -> ( Inv ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )