Theorem swapf2val

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

	Ref	Expression
Hypotheses	swapf1.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	swapf1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
	swapf1.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
	swapf2.z	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
	swapf2.w	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐷 ) )
	swapf2val.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapf2val.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
Assertion	swapf2val	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑍 , 𝑊 ⟩ ) = ( 𝑓 ∈ ( ⟨ 𝑋 , 𝑌 ⟩ 𝐻 ⟨ 𝑍 , 𝑊 ⟩ ) ↦ ∪ ◡ { 𝑓 } ) )

Proof

Step	Hyp	Ref	Expression
1		swapf1.o	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		swapf1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
3		swapf1.y	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
4		swapf2.z	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
5		swapf2.w	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐷 ) )
6		swapf2val.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
7		swapf2val.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
8		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
10	6 8 9	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑆 )
11	2 3	opelxpd	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
12	4 5	opelxpd	⊢ ( 𝜑 → ⟨ 𝑍 , 𝑊 ⟩ ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
13	1 6 10 11 12 7	swapf2vala	⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑍 , 𝑊 ⟩ ) = ( 𝑓 ∈ ( ⟨ 𝑋 , 𝑌 ⟩ 𝐻 ⟨ 𝑍 , 𝑊 ⟩ ) ↦ ∪ ◡ { 𝑓 } ) )