Metamath Proof Explorer

Theorem swapf2

Description: The morphism part of the swap functor swaps the morphisms. (Contributed by Zhi Wang, 7-Oct-2025)

Ref Expression
Hypotheses swapf1.o ⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
swapf1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
swapf1.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
swapf2.z ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
swapf2.w ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐷 ) )
swapf2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) )
swapf2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑊 ) )
Assertion swapf2 ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑍 , 𝑊 ⟩ ) 𝐺 ) = ⟨ 𝐺 , 𝐹 ⟩ )

Proof

Step Hyp Ref Expression
1 swapf1.o ⊢ ( 𝜑 → ( 𝐶 swapF 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2 swapf1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
3 swapf1.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
4 swapf2.z ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
5 swapf2.w ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐷 ) )
6 swapf2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) )
7 swapf2.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑊 ) )
8 df-ov ⊢ ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑍 , 𝑊 ⟩ ) 𝐺 ) = ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝐹 , 𝐺 ⟩ )
9 eqid ⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
10 eqidd ⊢ ( 𝜑 → ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) )
11 1 2 3 4 5 9 10 swapf2val ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑍 , 𝑊 ⟩ ) = ( 𝑓 ∈ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) ↦ ∪ ◡ { 𝑓 } ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ) → 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ )
13 12 sneqd ⊢ ( ( 𝜑 ∧ 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ) → { 𝑓 } = { ⟨ 𝐹 , 𝐺 ⟩ } )
14 13 cnveqd ⊢ ( ( 𝜑 ∧ 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ) → ◡ { 𝑓 } = ◡ { ⟨ 𝐹 , 𝐺 ⟩ } )
15 14 unieqd ⊢ ( ( 𝜑 ∧ 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ) → ∪ ◡ { 𝑓 } = ∪ ◡ { ⟨ 𝐹 , 𝐺 ⟩ } )
16 opswap ⊢ ∪ ◡ { ⟨ 𝐹 , 𝐺 ⟩ } = ⟨ 𝐺 , 𝐹 ⟩
17 15 16 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑓 = ⟨ 𝐹 , 𝐺 ⟩ ) → ∪ ◡ { 𝑓 } = ⟨ 𝐺 , 𝐹 ⟩ )
18 6 7 opelxpd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) × ( 𝑌 ( Hom ‘ 𝐷 ) 𝑊 ) ) )
19 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
20 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
21 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
22 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
23 eqid ⊢ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) = ( Hom ‘ ( 𝐶 ×c 𝐷 ) )
24 9 19 20 21 22 2 3 4 5 23 xpchom2 ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) = ( ( 𝑋 ( Hom ‘ 𝐶 ) 𝑍 ) × ( 𝑌 ( Hom ‘ 𝐷 ) 𝑊 ) ) )
25 18 24 eleqtrrd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ⟨ 𝑋 , 𝑌 ⟩ ( Hom ‘ ( 𝐶 ×c 𝐷 ) ) ⟨ 𝑍 , 𝑊 ⟩ ) )
26 opex ⊢ ⟨ 𝐺 , 𝐹 ⟩ ∈ V
27 26 a1i ⊢ ( 𝜑 → ⟨ 𝐺 , 𝐹 ⟩ ∈ V )
28 11 17 25 27 fvmptd ⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑍 , 𝑊 ⟩ ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ 𝐺 , 𝐹 ⟩ )
29 8 28 eqtrid ⊢ ( 𝜑 → ( 𝐹 ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑍 , 𝑊 ⟩ ) 𝐺 ) = ⟨ 𝐺 , 𝐹 ⟩ )