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	|- ( ph -> ( C swapF D ) = <. O , P >. )
	swapf1.x	|- ( ph -> X e. ( Base ` C ) )
	swapf1.y	|- ( ph -> Y e. ( Base ` D ) )
	swapf2.z	|- ( ph -> Z e. ( Base ` C ) )
	swapf2.w	|- ( ph -> W e. ( Base ` D ) )
	swapf2val.s	|- S = ( C Xc. D )
	swapf2val.h	|- ( ph -> H = ( Hom ` S ) )
Assertion	swapf2val	|- ( ph -> ( <. X , Y >. P <. Z , W >. ) = ( f e. ( <. X , Y >. H <. Z , W >. ) |-> U. `' { f } ) )

Proof

Step	Hyp	Ref	Expression
1		swapf1.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
2		swapf1.x	|- ( ph -> X e. ( Base ` C ) )
3		swapf1.y	|- ( ph -> Y e. ( Base ` D ) )
4		swapf2.z	|- ( ph -> Z e. ( Base ` C ) )
5		swapf2.w	|- ( ph -> W e. ( Base ` D ) )
6		swapf2val.s	|- S = ( C Xc. D )
7		swapf2val.h	|- ( ph -> H = ( Hom ` S ) )
8		eqid	|- ( Base ` C ) = ( Base ` C )
9		eqid	|- ( Base ` D ) = ( Base ` D )
10	6 8 9	xpcbas	|- ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` S )
11	2 3	opelxpd	|- ( ph -> <. X , Y >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
12	4 5	opelxpd	|- ( ph -> <. Z , W >. e. ( ( Base ` C ) X. ( Base ` D ) ) )
13	1 6 10 11 12 7	swapf2vala	|- ( ph -> ( <. X , Y >. P <. Z , W >. ) = ( f e. ( <. X , Y >. H <. Z , W >. ) |-> U. `' { f } ) )