Theorem swapfiso

Description: The swap functor is an isomorphism between product categories. (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	⊢ ( 𝜑 → 𝑇 ∈ 𝑈 )
	swapfiso.i	⊢ 𝐼 = ( Iso ‘ 𝐸 )
Assertion	swapfiso	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( 𝑆 𝐼 𝑇 ) )

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		swapfiso.i	⊢ 𝐼 = ( Iso ‘ 𝐸 )
10	1 2	swapfelvv	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( V × V ) )
11		1st2nd2	⊢ ( ( 𝐶 swapF 𝐷 ) ∈ ( V × V ) → ( 𝐶 swapF 𝐷 ) = ⟨ ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) , ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ⟩ )
12	10 11	syl	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) , ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ⟩ )
13	1 2 3 4 12	swapfffth	⊢ ( 𝜑 → ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) ( ( 𝑆 Full 𝑇 ) ∩ ( 𝑆 Faith 𝑇 ) ) ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) )
14		df-br	⊢ ( ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) ( ( 𝑆 Full 𝑇 ) ∩ ( 𝑆 Faith 𝑇 ) ) ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ↔ ⟨ ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) , ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ⟩ ∈ ( ( 𝑆 Full 𝑇 ) ∩ ( 𝑆 Faith 𝑇 ) ) )
15	13 14	sylib	⊢ ( 𝜑 → ⟨ ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) , ( 2nd ‘ ( 𝐶 swapF 𝐷 ) ) ⟩ ∈ ( ( 𝑆 Full 𝑇 ) ∩ ( 𝑆 Faith 𝑇 ) ) )
16	12 15	eqeltrd	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( ( 𝑆 Full 𝑇 ) ∩ ( 𝑆 Faith 𝑇 ) ) )
17		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
18		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
19	12 3 4 1 2 17 18	swapf1f1o	⊢ ( 𝜑 → ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) )
20		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
21	3 1 2	xpccat	⊢ ( 𝜑 → 𝑆 ∈ Cat )
22	7 21	elind	⊢ ( 𝜑 → 𝑆 ∈ ( 𝑈 ∩ Cat ) )
23	5 20 6	catcbas	⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
24	22 23	eleqtrrd	⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ 𝐸 ) )
25	4 2 1	xpccat	⊢ ( 𝜑 → 𝑇 ∈ Cat )
26	8 25	elind	⊢ ( 𝜑 → 𝑇 ∈ ( 𝑈 ∩ Cat ) )
27	26 23	eleqtrrd	⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ 𝐸 ) )
28	5 20 17 18 6 24 27 9	catciso	⊢ ( 𝜑 → ( ( 𝐶 swapF 𝐷 ) ∈ ( 𝑆 𝐼 𝑇 ) ↔ ( ( 𝐶 swapF 𝐷 ) ∈ ( ( 𝑆 Full 𝑇 ) ∩ ( 𝑆 Faith 𝑇 ) ) ∧ ( 1st ‘ ( 𝐶 swapF 𝐷 ) ) : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) ) ) )
29	16 19 28	mpbir2and	⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) ∈ ( 𝑆 𝐼 𝑇 ) )