Metamath Proof Explorer

Theorem invfn

Description: The function value of the function returning the inverses of a category is a function over the Cartesian square of the base set of the category. Simplifies isofn (see isofnALT ). (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion invfn ( 𝐶 ∈ Cat → ( Inv ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ovex ⊢ ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∈ V
2 1 inex1 ⊢ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ∈ V
3 2 a1i ⊢ ( ( 𝐶 ∈ Cat ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ∈ V )
4 3 ralrimivva ⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ∈ V )
5 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) )
6 5 fnmpo ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ∈ V → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
7 4 6 syl ⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
8 df-inv ⊢ Inv = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) )
9 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
10 fveq2 ⊢ ( 𝑐 = 𝐶 → ( Sect ‘ 𝑐 ) = ( Sect ‘ 𝐶 ) )
11 10 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) = ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) )
12 10 oveqd ⊢ ( 𝑐 = 𝐶 → ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) = ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) )
13 12 cnveqd ⊢ ( 𝑐 = 𝐶 → ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) = ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) )
14 11 13 ineq12d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) = ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) )
15 9 9 14 mpoeq123dv ⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑥 ( Sect ‘ 𝑐 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝑐 ) 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) )
16 id ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
17 fvex ⊢ ( Base ‘ 𝐶 ) ∈ V
18 17 17 pm3.2i ⊢ ( ( Base ‘ 𝐶 ) ∈ V ∧ ( Base ‘ 𝐶 ) ∈ V )
19 mpoexga ⊢ ( ( ( Base ‘ 𝐶 ) ∈ V ∧ ( Base ‘ 𝐶 ) ∈ V ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) ∈ V )
20 18 19 mp1i ⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) ∈ V )
21 8 15 16 20 fvmptd3 ⊢ ( 𝐶 ∈ Cat → ( Inv ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) )
22 21 fneq1d ⊢ ( 𝐶 ∈ Cat → ( ( Inv ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Sect ‘ 𝐶 ) 𝑦 ) ∩ ◡ ( 𝑦 ( Sect ‘ 𝐶 ) 𝑥 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
23 7 22 mpbird ⊢ ( 𝐶 ∈ Cat → ( Inv ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )