Metamath Proof Explorer

Theorem isofn

Description: The function value of the function returning the isomorphisms of a category is a function over the Cartesian square 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