Theorem swapffunca

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

	Ref	Expression
Hypotheses	swapfid.c	|- ( ph -> C e. Cat )
	swapfid.d	|- ( ph -> D e. Cat )
	swapfid.s	|- S = ( C Xc. D )
	swapfid.t	|- T = ( D Xc. C )
Assertion	swapffunca	|- ( ph -> ( C swapF D ) e. ( S Func T ) )

Proof

Step	Hyp	Ref	Expression
1		swapfid.c	|- ( ph -> C e. Cat )
2		swapfid.d	|- ( ph -> D e. Cat )
3		swapfid.s	|- S = ( C Xc. D )
4		swapfid.t	|- T = ( D Xc. C )
5	1 2	swapfelvv	|- ( ph -> ( C swapF D ) e. ( _V X. _V ) )
6		1st2nd2	|- ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. )
7	5 6	syl	|- ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. )
8	1 2 3 4 7	swapffunc	|- ( ph -> ( 1st ` ( C swapF D ) ) ( S Func T ) ( 2nd ` ( C swapF D ) ) )
9		df-br	|- ( ( 1st ` ( C swapF D ) ) ( S Func T ) ( 2nd ` ( C swapF D ) ) <-> <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. e. ( S Func T ) )
10	8 9	sylib	|- ( ph -> <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. e. ( S Func T ) )
11	7 10	eqeltrd	|- ( ph -> ( C swapF D ) e. ( S Func T ) )