Theorem swapf2fn

Description: The morphism part of the swap functor is a function on the Cartesian square of the base set. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	swapf2fvala.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapf2fvala.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	swapf1val.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
Assertion	swapf2fn	⊢ ( 𝜑 → 𝑃 Fn ( 𝐵 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
2		swapfval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
3		swapf2fvala.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
4		swapf2fvala.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
5		swapf1val.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
6		eqid	⊢ ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) )
7		ovex	⊢ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ∈ V
8	7	mptex	⊢ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ∈ V
9	6 8	fnmpoi	⊢ ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) Fn ( 𝐵 × 𝐵 )
10		eqidd	⊢ ( 𝜑 → ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 ) )
11	1 2 3 4 10 5	swapf2fval	⊢ ( 𝜑 → 𝑃 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) )
12	11	fneq1d	⊢ ( 𝜑 → ( 𝑃 Fn ( 𝐵 × 𝐵 ) ↔ ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑆 ) 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) Fn ( 𝐵 × 𝐵 ) ) )
13	9 12	mpbiri	⊢ ( 𝜑 → 𝑃 Fn ( 𝐵 × 𝐵 ) )