Metamath Proof Explorer

Theorem swapfid

Description: Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfida . (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 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
swapfid.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
swapfid.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
swapfid.1 ⊢ 1 = ( Id ‘ 𝑆 )
swapfid.i ⊢ 𝐼 = ( Id ‘ 𝑇 )
Assertion swapfid ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ‘ ( 1 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐼 ‘ ( 𝑂 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )

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 swapfid.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
7 swapfid.y ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
8 swapfid.1 ⊢ 1 = ( Id ‘ 𝑆 )
9 swapfid.i ⊢ 𝐼 = ( Id ‘ 𝑇 )
10 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
11 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
13 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
14 4 2 1 10 11 12 13 9 7 6 xpcid ⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑌 , 𝑋 ⟩ ) = ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ )
15 df-ov ⊢ ( 𝑋 𝑂 𝑌 ) = ( 𝑂 ‘ ⟨ 𝑋 , 𝑌 ⟩ )
16 5 6 7 swapf1 ⊢ ( 𝜑 → ( 𝑋 𝑂 𝑌 ) = ⟨ 𝑌 , 𝑋 ⟩ )
17 15 16 eqtr3id ⊢ ( 𝜑 → ( 𝑂 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ 𝑌 , 𝑋 ⟩ )
18 17 fveq2d ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑂 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐼 ‘ ⟨ 𝑌 , 𝑋 ⟩ ) )
19 3 1 2 11 10 13 12 8 6 7 xpcid ⊢ ( 𝜑 → ( 1 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) = ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ⟩ )
20 19 fveq2d ⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ‘ ( 1 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ⟩ ) )
21 df-ov ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ) = ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ⟩ )
22 21 a1i ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ) = ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ‘ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ⟩ ) )
23 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
24 11 23 13 1 6 catidcl ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
25 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
26 10 25 12 2 7 catidcl ⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑌 ) )
27 5 6 7 6 7 24 26 swapf2 ⊢ ( 𝜑 → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) ) = ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ )
28 20 22 27 3eqtr2d ⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ‘ ( 1 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ⟨ ( ( Id ‘ 𝐷 ) ‘ 𝑌 ) , ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ⟩ )
29 14 18 28 3eqtr4rd ⊢ ( 𝜑 → ( ( ⟨ 𝑋 , 𝑌 ⟩ 𝑃 ⟨ 𝑋 , 𝑌 ⟩ ) ‘ ( 1 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) = ( 𝐼 ‘ ( 𝑂 ‘ ⟨ 𝑋 , 𝑌 ⟩ ) ) )