Theorem swapf2fn

Description: The morphism part of the swap functor is a function on the Cartesian square of the base set. (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 )
	swapf1val.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
Assertion	swapf2fn	|- ( ph -> P Fn ( B X. B ) )

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		swapf1val.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
6		eqid	|- ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) = ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) )
7		ovex	|- ( u ( Hom ` S ) v ) e. _V
8	7	mptex	|- ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) e. _V
9	6 8	fnmpoi	|- ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) Fn ( B X. B )
10		eqidd	|- ( ph -> ( Hom ` S ) = ( Hom ` S ) )
11	1 2 3 4 10 5	swapf2fval	|- ( ph -> P = ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) )
12	11	fneq1d	|- ( ph -> ( P Fn ( B X. B ) <-> ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) Fn ( B X. B ) ) )
13	9 12	mpbiri	|- ( ph -> P Fn ( B X. B ) )