Theorem swapfffth

Description: The swap functor is a fully faithful 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	swapfffth	$$⊢\phi \to O\left(\left(S\mathrm{Full}T\right)\cap \left(S\mathrm{Faith}T\right)\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	1 2 3 4 5	swapffunc	$$⊢\phi \to O\left(S\mathrm{Func}T\right)P$$
7	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 |-
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{Base}}_S={\mathrm{Base}}_S$$
11		simprl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to x\in {\mathrm{Base}}_S$$
12		simprr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\right)\to y\in {\mathrm{Base}}_S$$
13	7 3 4 8 9 10 11 12	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)$$
14	13	ralrimivva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_S\forall y\in {\mathrm{Base}}_S\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)$$
15	10 8 9	isffth2	$$⊢O\left(\left(S\mathrm{Full}T\right)\cap \left(S\mathrm{Faith}T\right)\right)P\leftrightarrow \left(O\left(S\mathrm{Func}T\right)P\wedge \forall x\in {\mathrm{Base}}_S\forall y\in {\mathrm{Base}}_S\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)\right)$$
16	6 14 15	sylanbrc	$$⊢\phi \to O\left(\left(S\mathrm{Full}T\right)\cap \left(S\mathrm{Faith}T\right)\right)P$$