This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sectfn

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

Ref Expression
Assertion sectfn ( 𝐶 ∈ Cat → ( Sect ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } )
2 ovex ⊢ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∈ V
3 ovex ⊢ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ∈ V
4 2 3 xpex ⊢ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∈ V
5 opabssxp ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ⊆ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
6 4 5 ssexi ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ∈ V
7 1 6 fnmpoi ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
8 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
12 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
13 id ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat )
14 8 9 10 11 12 13 sectffval ⊢ ( 𝐶 ∈ Cat → ( Sect ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) )
15 14 fneq1d ⊢ ( 𝐶 ∈ Cat → ( ( Sect ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
16 7 15 mpbiri ⊢ ( 𝐶 ∈ Cat → ( Sect ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )