Metamath Proof Explorer

Theorem swapffunc

Description: The swap functor is a functor. (Contributed by Zhi Wang, 8-Oct-2025)

Ref Expression
Hypotheses swapfid.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
swapfid.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
swapfid.s ⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
swapfid.t ⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
swapfid.o ⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
Assertion swapffunc ( 𝜑 → 𝑂 ( 𝑆 Func 𝑇 ) 𝑃 )

Proof

Step Hyp Ref Expression
1 swapfid.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 swapfid.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
3 swapfid.s ⊢ 𝑆 = ( 𝐶 ×c 𝐷 )
4 swapfid.t ⊢ 𝑇 = ( 𝐷 ×c 𝐶 )
5 swapfid.o ⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
6 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
8 eqid ⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
9 eqid ⊢ ( Hom ‘ 𝑇 ) = ( Hom ‘ 𝑇 )
10 eqid ⊢ ( Id ‘ 𝑆 ) = ( Id ‘ 𝑆 )
11 eqid ⊢ ( Id ‘ 𝑇 ) = ( Id ‘ 𝑇 )
12 eqid ⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
13 eqid ⊢ ( comp ‘ 𝑇 ) = ( comp ‘ 𝑇 )
14 3 1 2 xpccat ⊢ ( 𝜑 → 𝑆 ∈ Cat )
15 4 2 1 xpccat ⊢ ( 𝜑 → 𝑇 ∈ Cat )
16 5 3 4 1 2 6 7 swapf1f1o ⊢ ( 𝜑 → 𝑂 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) )
17 f1of ⊢ ( 𝑂 : ( Base ‘ 𝑆 ) –1-1-onto→ ( Base ‘ 𝑇 ) → 𝑂 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
18 16 17 syl ⊢ ( 𝜑 → 𝑂 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
19 1 2 3 6 5 swapf2fn ⊢ ( 𝜑 → 𝑃 Fn ( ( Base ‘ 𝑆 ) × ( Base ‘ 𝑆 ) ) )
20 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
22 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
23 20 3 4 8 9 6 21 22 swapf2f1oa ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 𝑃 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑦 ) ) )
24 f1of ⊢ ( ( 𝑥 𝑃 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑦 ) ) → ( 𝑥 𝑃 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ⟶ ( ( 𝑂 ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑦 ) ) )
25 23 24 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) ) → ( 𝑥 𝑃 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ⟶ ( ( 𝑂 ‘ 𝑥 ) ( Hom ‘ 𝑇 ) ( 𝑂 ‘ 𝑦 ) ) )
26 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝐶 ∈ Cat )
27 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝐷 ∈ Cat )
28 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
30 26 27 3 4 28 6 29 10 11 swapfida ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑥 𝑃 𝑥 ) ‘ ( ( Id ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑇 ) ‘ ( 𝑂 ‘ 𝑥 ) ) )
31 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) ) ) → 𝐶 ∈ Cat )
32 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) ) ) → 𝐷 ∈ Cat )
33 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) ) ) → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
34 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
35 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
36 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑆 ) )
37 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) ) ) → 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) )
38 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) ) ) → 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) )
39 31 32 3 4 33 6 34 35 36 8 37 38 12 13 swapfcoa ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ 𝑧 ∈ ( Base ‘ 𝑆 ) ) ∧ ( 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑆 ) 𝑦 ) ∧ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑆 ) 𝑧 ) ) ) → ( ( 𝑥 𝑃 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑆 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑃 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑂 ‘ 𝑥 ) , ( 𝑂 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑇 ) ( 𝑂 ‘ 𝑧 ) ) ( ( 𝑥 𝑃 𝑦 ) ‘ 𝑚 ) ) )
40 6 7 8 9 10 11 12 13 14 15 18 19 25 30 39 isfuncd ⊢ ( 𝜑 → 𝑂 ( 𝑆 Func 𝑇 ) 𝑃 )