Theorem swapf2fvala

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

	Ref	Expression
Hypotheses	swapfval.c	|- ( ph -> C e. U )
	swapfval.d	|- ( ph -> D e. V )
	swapf2fvala.s	|- S = ( C Xc. D )
	swapf2fvala.b	|- B = ( Base ` S )
	swapf2fvala.h	|- ( ph -> H = ( Hom ` S ) )
Assertion	swapf2fvala	|- ( ph -> ( 2nd ` ( C swapF D ) ) = ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) )

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	|- ( ph -> C e. U )
2		swapfval.d	|- ( ph -> D e. V )
3		swapf2fvala.s	|- S = ( C Xc. D )
4		swapf2fvala.b	|- B = ( Base ` S )
5		swapf2fvala.h	|- ( ph -> H = ( Hom ` S ) )
6	1 2 3 4 5	swapfval	|- ( ph -> ( C swapF D ) = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. )
7	6	fveq2d	|- ( ph -> ( 2nd ` ( C swapF D ) ) = ( 2nd ` <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. ) )
8	4	fvexi	|- B e. _V
9	8	mptex	|- ( x e. B |-> U. `' { x } ) e. _V
10	8 8	mpoex	|- ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) e. _V
11	9 10	op2nd	|- ( 2nd ` <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) >. ) = ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) )
12	7 11	eqtrdi	|- ( ph -> ( 2nd ` ( C swapF D ) ) = ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) )