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	$$⊢\phi \to C\in \mathrm{Cat}$$
	swapfid.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	swapfid.s	$$⊢S=C{\times }_{c}D$$
	swapfid.t	$$⊢T=D{\times }_{c}C$$
	swapfid.o	No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
	swapfida.b	$$⊢B={\mathrm{Base}}_S$$
	swapfida.x	$$⊢\phi \to X\in B$$
	swapfida.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(S\right)$$
	swapfida.i	$$⊢I=\mathrm{Id}\left(T\right)$$
Assertion	swapfida	$$⊢\phi \to \left(XPX\right)\left(\underset{\dot{}}{1}\left(X\right)\right)=I\left(O\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		swapfid.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		swapfid.d	$$⊢\phi \to D\in \mathrm{Cat}$$
3		swapfid.s	$$⊢S=C{\times }_{c}D$$
4		swapfid.t	$$⊢T=D{\times }_{c}C$$
5		swapfid.o	Could not format ( ph -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
6		swapfida.b	$$⊢B={\mathrm{Base}}_S$$
7		swapfida.x	$$⊢\phi \to X\in B$$
8		swapfida.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(S\right)$$
9		swapfida.i	$$⊢I=\mathrm{Id}\left(T\right)$$
10		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
11		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
12	3 10 11	xpcbas	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_S$$
13	6 12	eqtr4i	$$⊢B={\mathrm{Base}}_C\times {\mathrm{Base}}_D$$
14	7 13	eleqtrdi	$$⊢\phi \to X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)$$
15		xp1st	$$⊢X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to 1^{st}\left(X\right)\in {\mathrm{Base}}_C$$
16	14 15	syl	$$⊢\phi \to 1^{st}\left(X\right)\in {\mathrm{Base}}_C$$
17		xp2nd	$$⊢X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to 2^{nd}\left(X\right)\in {\mathrm{Base}}_D$$
18	14 17	syl	$$⊢\phi \to 2^{nd}\left(X\right)\in {\mathrm{Base}}_D$$
19	1 2 3 4 5 16 18 8 9	swapfid	$$⊢\phi \to \left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩P⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\right)\left(\underset{\dot{}}{1}\left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\right)\right)=I\left(O\left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\right)\right)$$
20		1st2nd2	$$⊢X\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_D\right)\to X=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩$$
21	14 20	syl	$$⊢\phi \to X=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩$$
22	21 21	oveq12d	$$⊢\phi \to XPX=⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩P⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩$$
23	21	fveq2d	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)=\underset{\dot{}}{1}\left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\right)$$
24	22 23	fveq12d	$$⊢\phi \to \left(XPX\right)\left(\underset{\dot{}}{1}\left(X\right)\right)=\left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩P⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\right)\left(\underset{\dot{}}{1}\left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\right)\right)$$
25	21	fveq2d	$$⊢\phi \to O\left(X\right)=O\left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\right)$$
26	25	fveq2d	$$⊢\phi \to I\left(O\left(X\right)\right)=I\left(O\left(⟨1^{st}\left(X\right),2^{nd}\left(X\right)⟩\right)\right)$$
27	19 24 26	3eqtr4d	$$⊢\phi \to \left(XPX\right)\left(\underset{\dot{}}{1}\left(X\right)\right)=I\left(O\left(X\right)\right)$$