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	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	swapfid.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	swapfid.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
	swapfid.t	⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
	swapfiso.e	⊢ 𝐸 = ( CatCat ‘ 𝑈 )
	swapfiso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	swapfiso.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
	swapfiso.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑈 )
Assertion	swapciso	⊢ ( 𝜑 → 𝑆 ( ≃𝑐 ‘ 𝐸 ) 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		swapfid.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		swapfid.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		swapfid.s	⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
4		swapfid.t	⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
5		swapfiso.e	⊢ 𝐸 = ( CatCat ‘ 𝑈 )
6		swapfiso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
7		swapfiso.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑈 )
8		swapfiso.t	⊢ ( 𝜑 → 𝑇 ∈ 𝑈 )
9		eqid	⊢ ( Iso ‘ 𝐸 ) = ( Iso ‘ 𝐸 )
10		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
11	5	catccat	⊢ ( 𝑈 ∈ 𝑉 → 𝐸 ∈ Cat )
12	6 11	syl	⊢ ( 𝜑 → 𝐸 ∈ Cat )
13	3 1 2	xpccat	⊢ ( 𝜑 → 𝑆 ∈ Cat )
14	7 13	elind	⊢ ( 𝜑 → 𝑆 ∈ ( 𝑈 ∩ Cat ) )
15	5 10 6	catcbas	⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
16	14 15	eleqtrrd	⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ 𝐸 ) )
17	4 2 1	xpccat	⊢ ( 𝜑 → 𝑇 ∈ Cat )
18	8 17	elind	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑈 ∩ Cat ) )
19	18 15	eleqtrrd	⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ 𝐸 ) )
20	1 2 3 4 5 6 7 8 9	swapfiso	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( 𝑆 ( Iso ‘ 𝐸 ) 𝑇 ) )
21	9 10 12 16 19 20	brcici	⊢ ( 𝜑 → 𝑆 ( ≃𝑐 ‘ 𝐸 ) 𝑇 )