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	$$⊢\phi \to C\in U$$
	swapfval.d	$$⊢\phi \to D\in V$$
	swapf2fvala.s	$$⊢S=C{\times }_{c}D$$
	swapf2fvala.b	$$⊢B={\mathrm{Base}}_S$$
	swapf1val.o	No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
Assertion	swapf2fn	$$⊢\phi \to PFn\left(B\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	$$⊢\phi \to C\in U$$
2		swapfval.d	$$⊢\phi \to D\in V$$
3		swapf2fvala.s	$$⊢S=C{\times }_{c}D$$
4		swapf2fvala.b	$$⊢B={\mathrm{Base}}_S$$
5		swapf1val.o	Could not format ( ph -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
6		eqid	$$⊢\left(u\in B,v\in B⟼\left(f\in \left(u\mathrm{Hom}\left(S\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)=\left(u\in B,v\in B⟼\left(f\in \left(u\mathrm{Hom}\left(S\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)$$
7		ovex	$$⊢u\mathrm{Hom}\left(S\right)v\in \mathrm{V}$$
8	7	mptex	$$⊢\left(f\in \left(u\mathrm{Hom}\left(S\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\in \mathrm{V}$$
9	6 8	fnmpoi	$$⊢\left(u\in B,v\in B⟼\left(f\in \left(u\mathrm{Hom}\left(S\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)Fn\left(B\times B\right)$$
10		eqidd	$$⊢\phi \to \mathrm{Hom}\left(S\right)=\mathrm{Hom}\left(S\right)$$
11	1 2 3 4 10 5	swapf2fval	$$⊢\phi \to P=\left(u\in B,v\in B⟼\left(f\in \left(u\mathrm{Hom}\left(S\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)$$
12	11	fneq1d	$$⊢\phi \to \left(PFn\left(B\times B\right)\leftrightarrow \left(u\in B,v\in B⟼\left(f\in \left(u\mathrm{Hom}\left(S\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)Fn\left(B\times B\right)\right)$$
13	9 12	mpbiri	$$⊢\phi \to PFn\left(B\times B\right)$$