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 ‘ 𝐶 ) ) )