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⁡CFnBaseC×BaseC

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∈Vdom⁡x∈V
4 eqid ⊢x∈V⟼dom⁡x=x∈V⟼dom⁡x
5 4 fnmpt ⊢∀x∈Vdom⁡x∈V→x∈V⟼dom⁡xFnV
6 3 5 syl ⊢C∈Cat→x∈V⟼dom⁡xFnV
7 ovex ⊢xSect⁡Cy∈V
8 7 inex1 ⊢xSect⁡Cy∩ySect⁡Cx-1∈V
9 8 a1i ⊢C∈Cat∧x∈BaseC∧y∈BaseC→xSect⁡Cy∩ySect⁡Cx-1∈V
10 9 ralrimivva ⊢C∈Cat→∀x∈BaseC∀y∈BaseCxSect⁡Cy∩ySect⁡Cx-1∈V
11 eqid ⊢x∈BaseC,y∈BaseC⟼xSect⁡Cy∩ySect⁡Cx-1=x∈BaseC,y∈BaseC⟼xSect⁡Cy∩ySect⁡Cx-1
12 11 fnmpo ⊢∀x∈BaseC∀y∈BaseCxSect⁡Cy∩ySect⁡Cx-1∈V→x∈BaseC,y∈BaseC⟼xSect⁡Cy∩ySect⁡Cx-1FnBaseC×BaseC
13 10 12 syl ⊢C∈Cat→x∈BaseC,y∈BaseC⟼xSect⁡Cy∩ySect⁡Cx-1FnBaseC×BaseC
14 df-inv ⊢Inv=c∈Cat⟼x∈Basec,y∈Basec⟼xSect⁡cy∩ySect⁡cx-1
15 fveq2 ⊢c=C→Basec=BaseC
16 fveq2 ⊢c=C→Sect⁡c=Sect⁡C
17 16 oveqd ⊢c=C→xSect⁡cy=xSect⁡Cy
18 16 oveqd ⊢c=C→ySect⁡cx=ySect⁡Cx
19 18 cnveqd ⊢c=C→ySect⁡cx-1=ySect⁡Cx-1
20 17 19 ineq12d ⊢c=C→xSect⁡cy∩ySect⁡cx-1=xSect⁡Cy∩ySect⁡Cx-1
21 15 15 20 mpoeq123dv ⊢c=C→x∈Basec,y∈Basec⟼xSect⁡cy∩ySect⁡cx-1=x∈BaseC,y∈BaseC⟼xSect⁡Cy∩ySect⁡Cx-1
22 id ⊢C∈Cat→C∈Cat
23 fvex ⊢BaseC∈V
24 23 23 pm3.2i ⊢BaseC∈V∧BaseC∈V
25 mpoexga ⊢BaseC∈V∧BaseC∈V→x∈BaseC,y∈BaseC⟼xSect⁡Cy∩ySect⁡Cx-1∈V
26 24 25 mp1i ⊢C∈Cat→x∈BaseC,y∈BaseC⟼xSect⁡Cy∩ySect⁡Cx-1∈V
27 14 21 22 26 fvmptd3 ⊢C∈Cat→Inv⁡C=x∈BaseC,y∈BaseC⟼xSect⁡Cy∩ySect⁡Cx-1
28 27 fneq1d ⊢C∈Cat→Inv⁡CFnBaseC×BaseC↔x∈BaseC,y∈BaseC⟼xSect⁡Cy∩ySect⁡Cx-1FnBaseC×BaseC
29 13 28 mpbird ⊢C∈Cat→Inv⁡CFnBaseC×BaseC
30 ssv ⊢ran⁡Inv⁡C⊆V
31 30 a1i ⊢C∈Cat→ran⁡Inv⁡C⊆V
32 fnco ⊢x∈V⟼dom⁡xFnV∧Inv⁡CFnBaseC×BaseC∧ran⁡Inv⁡C⊆V→x∈V⟼dom⁡x∘Inv⁡CFnBaseC×BaseC
33 6 29 31 32 syl3anc ⊢C∈Cat→x∈V⟼dom⁡x∘Inv⁡CFnBaseC×BaseC
34 isofval ⊢C∈Cat→Iso⁡C=x∈V⟼dom⁡x∘Inv⁡C
35 34 fneq1d ⊢C∈Cat→Iso⁡CFnBaseC×BaseC↔x∈V⟼dom⁡x∘Inv⁡CFnBaseC×BaseC
36 33 35 mpbird ⊢C∈Cat→Iso⁡CFnBaseC×BaseC