Theorem swapf2vala

Description: The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	swapf1a.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	swapf1a.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapf1a.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	swapf1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	swapf2a.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	swapf2a.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
Assertion	swapf2vala	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ∪ ◡ { 𝑓 } ) )

Proof

Step	Hyp	Ref	Expression
1		swapf1a.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		swapf1a.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
3		swapf1a.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		swapf1a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		swapf2a.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		swapf2a.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
7	2 3 4	elxpcbasex1	⊢ ( 𝜑 → 𝐶 ∈ V )
8	2 3 4	elxpcbasex2	⊢ ( 𝜑 → 𝐷 ∈ V )
9	7 8 2 3 6 1	swapf2fval	⊢ ( 𝜑 → 𝑃 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) ) )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) ) → 𝑢 = 𝑋 )
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) ) → 𝑣 = 𝑌 )
12	10 11	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) ) → ( 𝑢 𝐻 𝑣 ) = ( 𝑋 𝐻 𝑌 ) )
13	12	mpteq1d	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑋 ∧ 𝑣 = 𝑌 ) ) → ( 𝑓 ∈ ( 𝑢 𝐻 𝑣 ) ↦ ∪ ◡ { 𝑓 } ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ∪ ◡ { 𝑓 } ) )
14		ovex	⊢ ( 𝑋 𝐻 𝑌 ) ∈ V
15	14	mptex	⊢ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ∪ ◡ { 𝑓 } ) ∈ V
16	15	a1i	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ∪ ◡ { 𝑓 } ) ∈ V )
17	9 13 4 5 16	ovmpod	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ∪ ◡ { 𝑓 } ) )