Theorem swapfida

Description: Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also swapfid . (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 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	swapfida.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	swapfida.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	swapfida.1	⊢ 1 = ( Id ‘ 𝑆 )
	swapfida.i	⊢ 𝐼 = ( Id ‘ 𝑇 )
Assertion	swapfida	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑋 ) ‘ ( 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		swapfida.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
7		swapfida.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		swapfida.1	⊢ 1 = ( Id ‘ 𝑆 )
9		swapfida.i	⊢ 𝐼 = ( Id ‘ 𝑇 )
10		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
11		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
12	3 10 11	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑆 )
13	6 12	eqtr4i	⊢ 𝐵 = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
14	7 13	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
15		xp1st	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 1st ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) )
16	14 15	syl	⊢ ( 𝜑 → ( 1st ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) )
17		xp2nd	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 2nd ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
18	14 17	syl	⊢ ( 𝜑 → ( 2nd ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
19	1 2 3 4 5 16 18 8 9	swapfid	⊢ ( 𝜑 → ( ( ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ 𝑃 ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) ‘ ( 1 ‘ ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) ) = ( 𝐼 ‘ ( 𝑂 ‘ ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) ) )
20		1st2nd2	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → 𝑋 = ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ )
21	14 20	syl	⊢ ( 𝜑 → 𝑋 = ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ )
22	21 21	oveq12d	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑋 ) = ( ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ 𝑃 ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) )
23	21	fveq2d	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( 1 ‘ ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) )
24	22 23	fveq12d	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) = ( ( ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ 𝑃 ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) ‘ ( 1 ‘ ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) ) )
25	21	fveq2d	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ( 𝑂 ‘ ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) )
26	25	fveq2d	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑂 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( 𝑂 ‘ ⟨ ( 1st ‘ 𝑋 ) , ( 2nd ‘ 𝑋 ) ⟩ ) ) )
27	19 24 26	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑋 ) ‘ ( 1 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( 𝑂 ‘ 𝑋 ) ) )