Theorem swapciso

Description: The product category is categorically isomorphic to the swapped product category. (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$$
Assertion	swapciso	$$⊢\phi \to S{\simeq }_{𝑐}\left(E\right)T$$

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		eqid	$$⊢\mathrm{Iso}\left(E\right)=\mathrm{Iso}\left(E\right)$$
10		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
11	5	catccat	$$⊢U\in V\to E\in \mathrm{Cat}$$
12	6 11	syl	$$⊢\phi \to E\in \mathrm{Cat}$$
13	3 1 2	xpccat	$$⊢\phi \to S\in \mathrm{Cat}$$
14	7 13	elind	$$⊢\phi \to S\in \left(U\cap \mathrm{Cat}\right)$$
15	5 10 6	catcbas	$$⊢\phi \to {\mathrm{Base}}_E=U\cap \mathrm{Cat}$$
16	14 15	eleqtrrd	$$⊢\phi \to S\in {\mathrm{Base}}_E$$
17	4 2 1	xpccat	$$⊢\phi \to T\in \mathrm{Cat}$$
18	8 17	elind	$$⊢\phi \to T\in \left(U\cap \mathrm{Cat}\right)$$
19	18 15	eleqtrrd	$$⊢\phi \to T\in {\mathrm{Base}}_E$$
20	1 2 3 4 5 6 7 8 9	swapfiso	Could not format ( ph -> ( C swapF D ) e. ( S ( Iso ` E ) T ) ) : No typesetting found for |- ( ph -> ( C swapF D ) e. ( S ( Iso ` E ) T ) ) with typecode |-
21	9 10 12 16 19 20	brcici	$$⊢\phi \to S{\simeq }_{𝑐}\left(E\right)T$$