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 Cat Iso C Fn Base C × Base C

Proof

Step Hyp Ref Expression
1 dmexg x V dom x V
2 1 adantl C Cat x V dom x V
3 2 ralrimiva C Cat x V dom x V
4 eqid x V dom x = x V dom x
5 4 fnmpt x V dom x V x V dom x Fn V
6 3 5 syl C Cat x V dom x Fn V
7 ovex x Sect C y V
8 7 inex1 x Sect C y y Sect C x -1 V
9 8 a1i C Cat x Base C y Base C x Sect C y y Sect C x -1 V
10 9 ralrimivva C Cat x Base C y Base C x Sect C y y Sect C x -1 V
11 eqid x Base C , y Base C x Sect C y y Sect C x -1 = x Base C , y Base C x Sect C y y Sect C x -1
12 11 fnmpo x Base C y Base C x Sect C y y Sect C x -1 V x Base C , y Base C x Sect C y y Sect C x -1 Fn Base C × Base C
13 10 12 syl C Cat x Base C , y Base C x Sect C y y Sect C x -1 Fn Base C × Base C
14 df-inv Inv = c Cat x Base c , y Base c x Sect c y y Sect c x -1
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 -1 = y Sect C x -1
20 17 19 ineq12d c = C x Sect c y y Sect c x -1 = x Sect C y y Sect C x -1
21 15 15 20 mpoeq123dv c = C x Base c , y Base c x Sect c y y Sect c x -1 = x Base C , y Base C x Sect C y y Sect C x -1
22 id C Cat C Cat
23 fvex Base C V
24 23 23 pm3.2i Base C V Base C V
25 mpoexga Base C V Base C V x Base C , y Base C x Sect C y y Sect C x -1 V
26 24 25 mp1i C Cat x Base C , y Base C x Sect C y y Sect C x -1 V
27 14 21 22 26 fvmptd3 C Cat Inv C = x Base C , y Base C x Sect C y y Sect C x -1
28 27 fneq1d C Cat Inv C Fn Base C × Base C x Base C , y Base C x Sect C y y Sect C x -1 Fn Base C × Base C
29 13 28 mpbird C Cat Inv C Fn Base C × Base C
30 ssv ran Inv C V
31 30 a1i C Cat ran Inv C V
32 fnco x V dom x Fn V Inv C Fn Base C × Base C ran Inv C V x V dom x Inv C Fn Base C × Base C
33 6 29 31 32 syl3anc C Cat x V dom x Inv C Fn Base C × Base C
34 isofval C Cat Iso C = x V dom x Inv C
35 34 fneq1d C Cat Iso C Fn Base C × Base C x V dom x Inv C Fn Base C × Base C
36 33 35 mpbird C Cat Iso C Fn Base C × Base C