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 ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 dmexg ⊢ ( 𝑥 ∈ V → dom 𝑥 ∈ V )
2 1 adantl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝑥 ∈ V ) → dom 𝑥 ∈ V )
3 2 ralrimiva ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ V dom 𝑥 ∈ V )
4 eqid ⊢ ( 𝑥 ∈ V ↦ dom 𝑥 ) = ( 𝑥 ∈ V ↦ dom 𝑥 )
5 4 fnmpt ⊢ ( ∀ 𝑥 ∈ V dom 𝑥 ∈ V → ( 𝑥 ∈ V ↦ dom 𝑥 ) Fn V )
6 3 5 syl ⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ V ↦ dom 𝑥 ) Fn V )
7 ovex ⊢ ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∈ V
8 7 inex1 ⊢ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ∈ V
9 8 a1i ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ∈ V )
10 9 ralrimivva ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ∈ V )
11 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) )
12 11 fnmpo ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ∈ V → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
13 10 12 syl ⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
14 df-inv ⊢ Inv = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) )
15 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
16 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Sect ‘ 𝑐 ) = ( Sect ‘ 𝐶 ) )
17 16 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) = ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) )
18 16 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) = ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) )
19 18 cnveqd ⊢ ( 𝑐 = 𝐶 → ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) = ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) )
20 17 19 ineq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) = ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) )
21 15 15 20 mpoeq123dv ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) )
22 id ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
23 fvex ⊢ ( Base ‘ 𝐶 ) ∈ V
24 23 23 pm3.2i ⊢ ( ( Base ‘ 𝐶 ) ∈ V ∧ ( Base ‘ 𝐶 ) ∈ V )
25 mpoexga ⊢ ( ( ( Base ‘ 𝐶 ) ∈ V ∧ ( Base ‘ 𝐶 ) ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) ∈ V )
26 24 25 mp1i ⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) ∈ V )
27 14 21 22 26 fvmptd3 ⊢ ( 𝐶 ∈ Cat → ( Inv ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) )
28 27 fneq1d ⊢ ( 𝐶 ∈ Cat → ( ( Inv ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
29 13 28 mpbird ⊢ ( 𝐶 ∈ Cat → ( Inv ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
30 ssv ⊢ ran ( Inv ‘ 𝐶 ) ⊆ V
31 30 a1i ⊢ ( 𝐶 ∈ Cat → ran ( Inv ‘ 𝐶 ) ⊆ V )
32 fnco ⊢ ( ( ( 𝑥 ∈ V ↦ dom 𝑥 ) Fn V ∧ ( Inv ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ran ( Inv ‘ 𝐶 ) ⊆ V ) → ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
33 6 29 31 32 syl3anc ⊢ ( 𝐶 ∈ Cat → ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
34 isofval ⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) = ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) )
35 34 fneq1d ⊢ ( 𝐶 ∈ Cat → ( ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( ( 𝑥 ∈ V ↦ dom 𝑥 ) ∘ ( Inv ‘ 𝐶 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
36 33 35 mpbird ⊢ ( 𝐶 ∈ Cat → ( Iso ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )