Metamath Proof Explorer

Theorem isofn

Description: The function value of the function returning the isomorphisms of a category is a function over the square product of the base set of the category. (Contributed by AV, 5-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 dmexg 
 |-  ( x e. _V -> dom x e. _V )
2 1 adantl 
 |-  ( ( C e. Cat /\ x e. _V ) -> dom x e. _V )
3 2 ralrimiva 
 |-  ( C e. Cat -> A. x e. _V dom x e. _V )
4 eqid 
 |-  ( x e. _V |-> dom x ) = ( x e. _V |-> dom x )
5 4 fnmpt 
 |-  ( A. x e. _V dom x e. _V -> ( x e. _V |-> dom x ) Fn _V )
6 3 5 syl 
 |-  ( C e. Cat -> ( x e. _V |-> dom x ) Fn _V )
7 ovex 
 |-  ( x ( Sect ` C ) y ) e. _V
8 7 inex1 
 |-  ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) e. _V
9 8 a1i 
 |-  ( ( C e. Cat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) e. _V )
10 9 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 )
11 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 ) ) )
12 11 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 ) ) )
13 10 12 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 ) ) )
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 fveq2 
 |-  ( c = C -> ( Base ` c ) = ( Base ` C ) )
16 fveq2 
 |-  ( c = C -> ( Sect ` c ) = ( Sect ` C ) )
17 16 oveqd 
 |-  ( c = C -> ( x ( Sect ` c ) y ) = ( x ( Sect ` C ) y ) )
18 16 oveqd 
 |-  ( c = C -> ( y ( Sect ` c ) x ) = ( y ( Sect ` C ) x ) )
19 18 cnveqd 
 |-  ( c = C -> `' ( y ( Sect ` c ) x ) = `' ( y ( Sect ` C ) x ) )
20 17 19 ineq12d 
 |-  ( c = C -> ( ( x ( Sect ` c ) y ) i^i `' ( y ( Sect ` c ) x ) ) = ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) )
21 15 15 20 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 ) ) ) )
22 id 
 |-  ( C e. Cat -> C e. Cat )
23 fvex 
 |-  ( Base ` C ) e. _V
24 23 23 pm3.2i 
 |-  ( ( Base ` C ) e. _V /\ ( Base ` C ) e. _V )
25 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 )
26 24 25 mp1i 
 |-  ( C e. Cat -> ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) e. _V )
27 14 21 22 26 fvmptd3 
 |-  ( C e. Cat -> ( Inv ` C ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Sect ` C ) y ) i^i `' ( y ( Sect ` C ) x ) ) ) )
28 27 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 ) ) ) )
29 13 28 mpbird 
 |-  ( C e. Cat -> ( Inv ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
30 ssv 
 |-  ran ( Inv ` C ) C_ _V
31 30 a1i 
 |-  ( C e. Cat -> ran ( Inv ` C ) C_ _V )
32 fnco 
 |-  ( ( ( x e. _V |-> dom x ) Fn _V /\ ( Inv ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ ran ( Inv ` C ) C_ _V ) -> ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
33 6 29 31 32 syl3anc 
 |-  ( C e. Cat -> ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
34 isofval 
 |-  ( C e. Cat -> ( Iso ` C ) = ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) )
35 34 fneq1d 
 |-  ( C e. Cat -> ( ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) <-> ( ( x e. _V |-> dom x ) o. ( Inv ` C ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) ) )
36 33 35 mpbird 
 |-  ( C e. Cat -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )