Theorem swapfiso

Description: The swap functor is an isomorphism between product categories. (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$$
	swapfiso.e	$$⊢E=\mathrm{CatCat}\left(U\right)$$
	swapfiso.u	$$⊢\phi \to U\in V$$
	swapfiso.s	$$⊢\phi \to S\in U$$
	swapfiso.t	$$⊢\phi \to T\in U$$
	swapfiso.i	$$⊢I=\mathrm{Iso}\left(E\right)$$
Assertion	swapfiso	Could not format assertion : No typesetting found for |- ( ph -> ( C swapF D ) e. ( S I T ) ) with typecode |-

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		swapfiso.e	$$⊢E=\mathrm{CatCat}\left(U\right)$$
6		swapfiso.u	$$⊢\phi \to U\in V$$
7		swapfiso.s	$$⊢\phi \to S\in U$$
8		swapfiso.t	$$⊢\phi \to T\in U$$
9		swapfiso.i	$$⊢I=\mathrm{Iso}\left(E\right)$$
10	1 2	swapfelvv	Could not format ( ph -> ( C swapF D ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( C swapF D ) e. ( _V X. _V ) ) with typecode |-
11		1st2nd2	Could not format ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) : No typesetting found for |- ( ( C swapF D ) e. ( _V X. _V ) -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) with typecode |-
12	10 11	syl	Could not format ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. ) with typecode |-
13	1 2 3 4 12	swapfffth	Could not format ( ph -> ( 1st ` ( C swapF D ) ) ( ( S Full T ) i^i ( S Faith T ) ) ( 2nd ` ( C swapF D ) ) ) : No typesetting found for |- ( ph -> ( 1st ` ( C swapF D ) ) ( ( S Full T ) i^i ( S Faith T ) ) ( 2nd ` ( C swapF D ) ) ) with typecode |-
14		df-br	Could not format ( ( 1st ` ( C swapF D ) ) ( ( S Full T ) i^i ( S Faith T ) ) ( 2nd ` ( C swapF D ) ) <-> <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. e. ( ( S Full T ) i^i ( S Faith T ) ) ) : No typesetting found for |- ( ( 1st ` ( C swapF D ) ) ( ( S Full T ) i^i ( S Faith T ) ) ( 2nd ` ( C swapF D ) ) <-> <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. e. ( ( S Full T ) i^i ( S Faith T ) ) ) with typecode |-
15	13 14	sylib	Could not format ( ph -> <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. e. ( ( S Full T ) i^i ( S Faith T ) ) ) : No typesetting found for |- ( ph -> <. ( 1st ` ( C swapF D ) ) , ( 2nd ` ( C swapF D ) ) >. e. ( ( S Full T ) i^i ( S Faith T ) ) ) with typecode |-
16	12 15	eqeltrd	Could not format ( ph -> ( C swapF D ) e. ( ( S Full T ) i^i ( S Faith T ) ) ) : No typesetting found for |- ( ph -> ( C swapF D ) e. ( ( S Full T ) i^i ( S Faith T ) ) ) with typecode |-
17		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
18		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
19	12 3 4 1 2 17 18	swapf1f1o	Could not format ( ph -> ( 1st ` ( C swapF D ) ) : ( Base ` S ) -1-1-onto-> ( Base ` T ) ) : No typesetting found for |- ( ph -> ( 1st ` ( C swapF D ) ) : ( Base ` S ) -1-1-onto-> ( Base ` T ) ) with typecode |-
20		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
21	3 1 2	xpccat	$$⊢\phi \to S\in \mathrm{Cat}$$
22	7 21	elind	$$⊢\phi \to S\in \left(U\cap \mathrm{Cat}\right)$$
23	5 20 6	catcbas	$$⊢\phi \to {\mathrm{Base}}_E=U\cap \mathrm{Cat}$$
24	22 23	eleqtrrd	$$⊢\phi \to S\in {\mathrm{Base}}_E$$
25	4 2 1	xpccat	$$⊢\phi \to T\in \mathrm{Cat}$$
26	8 25	elind	$$⊢\phi \to T\in \left(U\cap \mathrm{Cat}\right)$$
27	26 23	eleqtrrd	$$⊢\phi \to T\in {\mathrm{Base}}_E$$
28	5 20 17 18 6 24 27 9	catciso	Could not format ( ph -> ( ( C swapF D ) e. ( S I T ) <-> ( ( C swapF D ) e. ( ( S Full T ) i^i ( S Faith T ) ) /\ ( 1st ` ( C swapF D ) ) : ( Base ` S ) -1-1-onto-> ( Base ` T ) ) ) ) : No typesetting found for |- ( ph -> ( ( C swapF D ) e. ( S I T ) <-> ( ( C swapF D ) e. ( ( S Full T ) i^i ( S Faith T ) ) /\ ( 1st ` ( C swapF D ) ) : ( Base ` S ) -1-1-onto-> ( Base ` T ) ) ) ) with typecode |-
29	16 19 28	mpbir2and	Could not format ( ph -> ( C swapF D ) e. ( S I T ) ) : No typesetting found for |- ( ph -> ( C swapF D ) e. ( S I T ) ) with typecode |-