Theorem swapffunca

Description: The swap functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Hypotheses	swapfid.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	swapfid.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	swapfid.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapfid.t	⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
Assertion	swapffunca	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( 𝑆 Func 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		swapfid.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		swapfid.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		swapfid.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
4		swapfid.t	⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
5	1 2	swapfelvv	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( V × V ) )
6		1st2nd2	⊢ ( ( 𝐶 swapF 𝐷 ) ∈ ( V × V ) → ( 𝐶 swapF 𝐷 ) = ⟨ ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) , ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ⟩ )
7	5 6	syl	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) , ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ⟩ )
8	1 2 3 4 7	swapffunc	⊢ ( 𝜑 → ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) ( 𝑆 Func 𝑇 ) ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) )
9		df-br	⊢ ( ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) ( 𝑆 Func 𝑇 ) ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ↔ ⟨ ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) , ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ⟩ ∈ ( 𝑆 Func 𝑇 ) )
10	8 9	sylib	⊢ ( 𝜑 → ⟨ ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) , ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ⟩ ∈ ( 𝑆 Func 𝑇 ) )
11	7 10	eqeltrd	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( 𝑆 Func 𝑇 ) )