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	|- ( ph -> C e. Cat )
	swapfid.d	|- ( ph -> D e. Cat )
	swapfid.s	|- S = ( C Xc. D )
	swapfid.t	|- T = ( D Xc. C )
	swapfiso.e	|- E = ( CatCat ` U )
	swapfiso.u	|- ( ph -> U e. V )
	swapfiso.s	|- ( ph -> S e. U )
	swapfiso.t	|- ( ph -> T e. U )
Assertion	swapciso	|- ( ph -> S ( ~=c ` E ) T )

Proof

Step	Hyp	Ref	Expression
1		swapfid.c	|- ( ph -> C e. Cat )
2		swapfid.d	|- ( ph -> D e. Cat )
3		swapfid.s	|- S = ( C Xc. D )
4		swapfid.t	|- T = ( D Xc. C )
5		swapfiso.e	|- E = ( CatCat ` U )
6		swapfiso.u	|- ( ph -> U e. V )
7		swapfiso.s	|- ( ph -> S e. U )
8		swapfiso.t	|- ( ph -> T e. U )
9		eqid	|- ( Iso ` E ) = ( Iso ` E )
10		eqid	|- ( Base ` E ) = ( Base ` E )
11	5	catccat	|- ( U e. V -> E e. Cat )
12	6 11	syl	|- ( ph -> E e. Cat )
13	3 1 2	xpccat	|- ( ph -> S e. Cat )
14	7 13	elind	|- ( ph -> S e. ( U i^i Cat ) )
15	5 10 6	catcbas	|- ( ph -> ( Base ` E ) = ( U i^i Cat ) )
16	14 15	eleqtrrd	|- ( ph -> S e. ( Base ` E ) )
17	4 2 1	xpccat	|- ( ph -> T e. Cat )
18	8 17	elind	|- ( ph -> T e. ( U i^i Cat ) )
19	18 15	eleqtrrd	|- ( ph -> T e. ( Base ` E ) )
20	1 2 3 4 5 6 7 8 9	swapfiso	|- ( ph -> ( C swapF D ) e. ( S ( Iso ` E ) T ) )
21	9 10 12 16 19 20	brcici	|- ( ph -> S ( ~=c ` E ) T )