Theorem swapffunc

Description: The swap functor is a functor. (Contributed by Zhi Wang, 8-Oct-2025)

	Ref	Expression
Hypotheses	swapfid.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	swapfid.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	swapfid.s	$$⊢S=C{\times }_{c}D$$
	swapfid.t	$$⊢T=D{\times }_{c}C$$
	swapfid.o	No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
Assertion	swapffunc	$$⊢\phi \to O\left(S\mathrm{Func}T\right)P$$

Proof

Step	Hyp	Ref	Expression
1		swapfid.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		swapfid.d	$$⊢\phi \to D\in \mathrm{Cat}$$
3		swapfid.s	$$⊢S=C{\times }_{c}D$$
4		swapfid.t	$$⊢T=D{\times }_{c}C$$
5		swapfid.o	Could not format ( ph -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
6		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
7		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
8		eqid	$$⊢\mathrm{Hom}\left(S\right)=\mathrm{Hom}\left(S\right)$$
9		eqid	$$⊢\mathrm{Hom}\left(T\right)=\mathrm{Hom}\left(T\right)$$
10		eqid	$$⊢\mathrm{Id}\left(S\right)=\mathrm{Id}\left(S\right)$$
11		eqid	$$⊢\mathrm{Id}\left(T\right)=\mathrm{Id}\left(T\right)$$
12		eqid	$$⊢\mathrm{comp}\left(S\right)=\mathrm{comp}\left(S\right)$$
13		eqid	$$⊢\mathrm{comp}\left(T\right)=\mathrm{comp}\left(T\right)$$
14	3 1 2	xpccat	$$⊢\phi \to S\in \mathrm{Cat}$$
15	4 2 1	xpccat	$$⊢\phi \to T\in \mathrm{Cat}$$
16	5 3 4 1 2 6 7	swapf1f1o	$$⊢\phi \to O:{\mathrm{Base}}_S\underset{1-1\; onto}{⟶}{\mathrm{Base}}_T$$
17		f1of	$$⊢O:{\mathrm{Base}}_S\underset{1-1\; onto}{⟶}{\mathrm{Base}}_T\to O:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T$$
18	16 17	syl	$$⊢\phi \to O:{\mathrm{Base}}_S⟶{\mathrm{Base}}_T$$
19	1 2 3 6 5	swapf2fn	$$⊢\phi \to PFn\left({\mathrm{Base}}_S\times {\mathrm{Base}}_S\right)$$
20	5	adantr	Could not format ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( C swapF D ) = <. O , P >. ) with typecode |-
21		simprl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to x\in {\mathrm{Base}}_S$$
22		simprr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to y\in {\mathrm{Base}}_S$$
23	20 3 4 8 9 6 21 22	swapf2f1oa	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to \left(xPy\right):x\mathrm{Hom}\left(S\right)y\underset{1-1\; onto}{⟶}O\left(x\right)\mathrm{Hom}\left(T\right)O\left(y\right)$$
24		f1of	$$⊢\left(xPy\right):x\mathrm{Hom}\left(S\right)y\underset{1-1\; onto}{⟶}O\left(x\right)\mathrm{Hom}\left(T\right)O\left(y\right)\to \left(xPy\right):x\mathrm{Hom}\left(S\right)y⟶O\left(x\right)\mathrm{Hom}\left(T\right)O\left(y\right)$$
25	23 24	syl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to \left(xPy\right):x\mathrm{Hom}\left(S\right)y⟶O\left(x\right)\mathrm{Hom}\left(T\right)O\left(y\right)$$
26	1	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to C\in \mathrm{Cat}$$
27	2	adantr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to D\in \mathrm{Cat}$$
28	5	adantr	Could not format ( ( ph /\ x e. ( Base ` S ) ) -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ( ph /\ x e. ( Base ` S ) ) -> ( C swapF D ) = <. O , P >. ) with typecode |-
29		simpr	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to x\in {\mathrm{Base}}_S$$
30	26 27 3 4 28 6 29 10 11	swapfida	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_S\right)\to \left(xPx\right)\left(\mathrm{Id}\left(S\right)\left(x\right)\right)=\mathrm{Id}\left(T\right)\left(O\left(x\right)\right)$$
31	1	3ad2ant1	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\wedge \left(m\in \left(x\mathrm{Hom}\left(S\right)y\right)\wedge n\in \left(y\mathrm{Hom}\left(S\right)z\right)\right)\right)\to C\in \mathrm{Cat}$$
32	2	3ad2ant1	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\wedge \left(m\in \left(x\mathrm{Hom}\left(S\right)y\right)\wedge n\in \left(y\mathrm{Hom}\left(S\right)z\right)\right)\right)\to D\in \mathrm{Cat}$$
33	5	3ad2ant1	Could not format ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) /\ ( m e. ( x ( Hom ` S ) y ) /\ n e. ( y ( Hom ` S ) z ) ) ) -> ( C swapF D ) = <. O , P >. ) with typecode |-
34		simp21	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\wedge \left(m\in \left(x\mathrm{Hom}\left(S\right)y\right)\wedge n\in \left(y\mathrm{Hom}\left(S\right)z\right)\right)\right)\to x\in {\mathrm{Base}}_S$$
35		simp22	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\wedge \left(m\in \left(x\mathrm{Hom}\left(S\right)y\right)\wedge n\in \left(y\mathrm{Hom}\left(S\right)z\right)\right)\right)\to y\in {\mathrm{Base}}_S$$
36		simp23	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\wedge \left(m\in \left(x\mathrm{Hom}\left(S\right)y\right)\wedge n\in \left(y\mathrm{Hom}\left(S\right)z\right)\right)\right)\to z\in {\mathrm{Base}}_S$$
37		simp3l	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\wedge \left(m\in \left(x\mathrm{Hom}\left(S\right)y\right)\wedge n\in \left(y\mathrm{Hom}\left(S\right)z\right)\right)\right)\to m\in \left(x\mathrm{Hom}\left(S\right)y\right)$$
38		simp3r	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\wedge \left(m\in \left(x\mathrm{Hom}\left(S\right)y\right)\wedge n\in \left(y\mathrm{Hom}\left(S\right)z\right)\right)\right)\to n\in \left(y\mathrm{Hom}\left(S\right)z\right)$$
39	31 32 3 4 33 6 34 35 36 8 37 38 12 13	swapfcoa	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\wedge z\in {\mathrm{Base}}_S\right)\wedge \left(m\in \left(x\mathrm{Hom}\left(S\right)y\right)\wedge n\in \left(y\mathrm{Hom}\left(S\right)z\right)\right)\right)\to \left(xPz\right)\left(n\left(⟨x,y⟩\mathrm{comp}\left(S\right)z\right)m\right)=\left(yPz\right)\left(n\right)\left(⟨O\left(x\right),O\left(y\right)⟩\mathrm{comp}\left(T\right)O\left(z\right)\right)\left(xPy\right)\left(m\right)$$
40	6 7 8 9 10 11 12 13 14 15 18 19 25 30 39	isfuncd	$$⊢\phi \to O\left(S\mathrm{Func}T\right)P$$