Theorem swapf2a

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 ‘ 𝑆 ) )
	swapf2a.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
Assertion	swapf2a	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐹 ) = ⟨ ( 2nd ‘ 𝐹 ) , ( 1st ‘ 𝐹 ) ⟩ )

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		swapf2a.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
8	1 2 3 4 5 6	swapf2vala	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ∪ ◡ { 𝑓 } ) )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 )
10	9	sneqd	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → { 𝑓 } = { 𝐹 } )
11	10	cnveqd	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ◡ { 𝑓 } = ◡ { 𝐹 } )
12	11	unieqd	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ∪ ◡ { 𝑓 } = ∪ ◡ { 𝐹 } )
13	6	oveqd	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) )
14		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
15		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
16		eqid	⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
17	2 3 14 15 16 4 5	xpchom	⊢ ( 𝜑 → ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) = ( ( ( 1st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑌 ) ) ) )
18	13 17	eqtrd	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( ( ( 1st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑌 ) ) ) )
19	7 18	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( ( ( 1st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑌 ) ) ) )
20		2nd1st	⊢ ( 𝐹 ∈ ( ( ( 1st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1st ‘ 𝑌 ) ) × ( ( 2nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2nd ‘ 𝑌 ) ) ) → ∪ ◡ { 𝐹 } = ⟨ ( 2nd ‘ 𝐹 ) , ( 1st ‘ 𝐹 ) ⟩ )
21	19 20	syl	⊢ ( 𝜑 → ∪ ◡ { 𝐹 } = ⟨ ( 2nd ‘ 𝐹 ) , ( 1st ‘ 𝐹 ) ⟩ )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ∪ ◡ { 𝐹 } = ⟨ ( 2nd ‘ 𝐹 ) , ( 1st ‘ 𝐹 ) ⟩ )
23	12 22	eqtrd	⊢ ( ( 𝜑 ∧ 𝑓 = 𝐹 ) → ∪ ◡ { 𝑓 } = ⟨ ( 2nd ‘ 𝐹 ) , ( 1st ‘ 𝐹 ) ⟩ )
24		opex	⊢ ⟨ ( 2nd ‘ 𝐹 ) , ( 1st ‘ 𝐹 ) ⟩ ∈ V
25	24	a1i	⊢ ( 𝜑 → ⟨ ( 2nd ‘ 𝐹 ) , ( 1st ‘ 𝐹 ) ⟩ ∈ V )
26	8 23 7 25	fvmptd	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑌 ) ‘ 𝐹 ) = ⟨ ( 2nd ‘ 𝐹 ) , ( 1st ‘ 𝐹 ) ⟩ )