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	$$⊢\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 |-
	swapfid.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
	swapfid.y	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
	swapfid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(S\right)$$
	swapfid.i	$$⊢I=\mathrm{Id}\left(T\right)$$
Assertion	swapfid	$$⊢\phi \to \left(⟨X,Y⟩P⟨X,Y⟩\right)\left(\underset{\dot{}}{1}\left(⟨X,Y⟩\right)\right)=I\left(O\left(⟨X,Y⟩\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		swapfid.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
7		swapfid.y	$$⊢\phi \to Y\in {\mathrm{Base}}_D$$
8		swapfid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(S\right)$$
9		swapfid.i	$$⊢I=\mathrm{Id}\left(T\right)$$
10		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
11		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
12		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
13		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
14	4 2 1 10 11 12 13 9 7 6	xpcid	$$⊢\phi \to I\left(⟨Y,X⟩\right)=⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩$$
15		df-ov	$$⊢XOY=O\left(⟨X,Y⟩\right)$$
16	5 6 7	swapf1	$$⊢\phi \to XOY=⟨Y,X⟩$$
17	15 16	eqtr3id	$$⊢\phi \to O\left(⟨X,Y⟩\right)=⟨Y,X⟩$$
18	17	fveq2d	$$⊢\phi \to I\left(O\left(⟨X,Y⟩\right)\right)=I\left(⟨Y,X⟩\right)$$
19	3 1 2 11 10 13 12 8 6 7	xpcid	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨X,Y⟩\right)=⟨\mathrm{Id}\left(C\right)\left(X\right),\mathrm{Id}\left(D\right)\left(Y\right)⟩$$
20	19	fveq2d	$$⊢\phi \to \left(⟨X,Y⟩P⟨X,Y⟩\right)\left(\underset{\dot{}}{1}\left(⟨X,Y⟩\right)\right)=\left(⟨X,Y⟩P⟨X,Y⟩\right)\left(⟨\mathrm{Id}\left(C\right)\left(X\right),\mathrm{Id}\left(D\right)\left(Y\right)⟩\right)$$
21		df-ov	$$⊢\mathrm{Id}\left(C\right)\left(X\right)\left(⟨X,Y⟩P⟨X,Y⟩\right)\mathrm{Id}\left(D\right)\left(Y\right)=\left(⟨X,Y⟩P⟨X,Y⟩\right)\left(⟨\mathrm{Id}\left(C\right)\left(X\right),\mathrm{Id}\left(D\right)\left(Y\right)⟩\right)$$
22	21	a1i	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(X\right)\left(⟨X,Y⟩P⟨X,Y⟩\right)\mathrm{Id}\left(D\right)\left(Y\right)=\left(⟨X,Y⟩P⟨X,Y⟩\right)\left(⟨\mathrm{Id}\left(C\right)\left(X\right),\mathrm{Id}\left(D\right)\left(Y\right)⟩\right)$$
23		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
24	11 23 13 1 6	catidcl	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(X\right)\in \left(X\mathrm{Hom}\left(C\right)X\right)$$
25		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
26	10 25 12 2 7	catidcl	$$⊢\phi \to \mathrm{Id}\left(D\right)\left(Y\right)\in \left(Y\mathrm{Hom}\left(D\right)Y\right)$$
27	5 6 7 6 7 24 26	swapf2	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(X\right)\left(⟨X,Y⟩P⟨X,Y⟩\right)\mathrm{Id}\left(D\right)\left(Y\right)=⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩$$
28	20 22 27	3eqtr2d	$$⊢\phi \to \left(⟨X,Y⟩P⟨X,Y⟩\right)\left(\underset{\dot{}}{1}\left(⟨X,Y⟩\right)\right)=⟨\mathrm{Id}\left(D\right)\left(Y\right),\mathrm{Id}\left(C\right)\left(X\right)⟩$$
29	14 18 28	3eqtr4rd	$$⊢\phi \to \left(⟨X,Y⟩P⟨X,Y⟩\right)\left(\underset{\dot{}}{1}\left(⟨X,Y⟩\right)\right)=I\left(O\left(⟨X,Y⟩\right)\right)$$