Theorem swapf2vala

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

	Ref	Expression
Hypotheses	swapf1a.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
	swapf1a.s	|- S = ( C Xc. D )
	swapf1a.b	|- B = ( Base ` S )
	swapf1a.x	|- ( ph -> X e. B )
	swapf2a.y	|- ( ph -> Y e. B )
	swapf2a.h	|- ( ph -> H = ( Hom ` S ) )
Assertion	swapf2vala	|- ( ph -> ( X P Y ) = ( f e. ( X H Y ) |-> U. `' { f } ) )

Proof

Step	Hyp	Ref	Expression
1		swapf1a.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
2		swapf1a.s	|- S = ( C Xc. D )
3		swapf1a.b	|- B = ( Base ` S )
4		swapf1a.x	|- ( ph -> X e. B )
5		swapf2a.y	|- ( ph -> Y e. B )
6		swapf2a.h	|- ( ph -> H = ( Hom ` S ) )
7	2 3 4	elxpcbasex1	|- ( ph -> C e. _V )
8	2 3 4	elxpcbasex2	|- ( ph -> D e. _V )
9	7 8 2 3 6 1	swapf2fval	|- ( ph -> P = ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) )
10		simprl	|- ( ( ph /\ ( u = X /\ v = Y ) ) -> u = X )
11		simprr	|- ( ( ph /\ ( u = X /\ v = Y ) ) -> v = Y )
12	10 11	oveq12d	|- ( ( ph /\ ( u = X /\ v = Y ) ) -> ( u H v ) = ( X H Y ) )
13	12	mpteq1d	|- ( ( ph /\ ( u = X /\ v = Y ) ) -> ( f e. ( u H v ) |-> U. `' { f } ) = ( f e. ( X H Y ) |-> U. `' { f } ) )
14		ovex	|- ( X H Y ) e. _V
15	14	mptex	|- ( f e. ( X H Y ) |-> U. `' { f } ) e. _V
16	15	a1i	|- ( ph -> ( f e. ( X H Y ) |-> U. `' { f } ) e. _V )
17	9 13 4 5 16	ovmpod	|- ( ph -> ( X P Y ) = ( f e. ( X H Y ) |-> U. `' { f } ) )