Theorem swapf2fval

Description: The morphism part of the swap functor. See also swapf2fvala . (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 ) )
	swapf2fval.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
Assertion	swapf2fval	|- ( ph -> P = ( 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		swapf2fval.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
7	6	fveq2d	|- ( ph -> ( 2nd ` ( C swapF D ) ) = ( 2nd ` <. O , P >. ) )
8	1 2 3 4 5	swapf2fvala	|- ( ph -> ( 2nd ` ( C swapF D ) ) = ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) )
9	1 2	swapfelvv	|- ( ph -> ( C swapF D ) e. ( _V X. _V ) )
10	6 9	eqeltrrd	|- ( ph -> <. O , P >. e. ( _V X. _V ) )
11		opelxp	|- ( <. O , P >. e. ( _V X. _V ) <-> ( O e. _V /\ P e. _V ) )
12	11	biimpi	|- ( <. O , P >. e. ( _V X. _V ) -> ( O e. _V /\ P e. _V ) )
13		op2ndg	|- ( ( O e. _V /\ P e. _V ) -> ( 2nd ` <. O , P >. ) = P )
14	10 12 13	3syl	|- ( ph -> ( 2nd ` <. O , P >. ) = P )
15	7 8 14	3eqtr3rd	|- ( ph -> P = ( u e. B , v e. B |-> ( f e. ( u H v ) |-> U. `' { f } ) ) )