Theorem xpcid

Description: The identity morphism in the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpccat.t	$$⊢T=C{\times }_{c}D$$
	xpccat.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	xpccat.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	xpccat.x	$$⊢X={\mathrm{Base}}_C$$
	xpccat.y	$$⊢Y={\mathrm{Base}}_D$$
	xpccat.i	$$⊢I=\mathrm{Id}\left(C\right)$$
	xpccat.j	$$⊢J=\mathrm{Id}\left(D\right)$$
	xpcid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(T\right)$$
	xpcid.r	$$⊢\phi \to R\in X$$
	xpcid.s	$$⊢\phi \to S\in Y$$
Assertion	xpcid	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨R,S⟩\right)=⟨I\left(R\right),J\left(S\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		xpccat.t	$$⊢T=C{\times }_{c}D$$
2		xpccat.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		xpccat.d	$$⊢\phi \to D\in \mathrm{Cat}$$
4		xpccat.x	$$⊢X={\mathrm{Base}}_C$$
5		xpccat.y	$$⊢Y={\mathrm{Base}}_D$$
6		xpccat.i	$$⊢I=\mathrm{Id}\left(C\right)$$
7		xpccat.j	$$⊢J=\mathrm{Id}\left(D\right)$$
8		xpcid.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(T\right)$$
9		xpcid.r	$$⊢\phi \to R\in X$$
10		xpcid.s	$$⊢\phi \to S\in Y$$
11		df-ov	$$⊢R\underset{\dot{}}{1}S=\underset{\dot{}}{1}\left(⟨R,S⟩\right)$$
12	1 2 3 4 5 6 7	xpccatid	$$⊢\phi \to \left(T\in \mathrm{Cat}\wedge \mathrm{Id}\left(T\right)=\left(x\in X,y\in Y⟼⟨I\left(x\right),J\left(y\right)⟩\right)\right)$$
13	12	simprd	$$⊢\phi \to \mathrm{Id}\left(T\right)=\left(x\in X,y\in Y⟼⟨I\left(x\right),J\left(y\right)⟩\right)$$
14	8 13	syl5eq	$$⊢\phi \to \underset{\dot{}}{1}=\left(x\in X,y\in Y⟼⟨I\left(x\right),J\left(y\right)⟩\right)$$
15		simprl	$$⊢\left(\phi \wedge \left(x=R\wedge y=S\right)\right)\to x=R$$
16	15	fveq2d	$$⊢\left(\phi \wedge \left(x=R\wedge y=S\right)\right)\to I\left(x\right)=I\left(R\right)$$
17		simprr	$$⊢\left(\phi \wedge \left(x=R\wedge y=S\right)\right)\to y=S$$
18	17	fveq2d	$$⊢\left(\phi \wedge \left(x=R\wedge y=S\right)\right)\to J\left(y\right)=J\left(S\right)$$
19	16 18	opeq12d	$$⊢\left(\phi \wedge \left(x=R\wedge y=S\right)\right)\to ⟨I\left(x\right),J\left(y\right)⟩=⟨I\left(R\right),J\left(S\right)⟩$$
20		opex	$$⊢⟨I\left(R\right),J\left(S\right)⟩\in \mathrm{V}$$
21	20	a1i	$$⊢\phi \to ⟨I\left(R\right),J\left(S\right)⟩\in \mathrm{V}$$
22	14 19 9 10 21	ovmpod	$$⊢\phi \to R\underset{\dot{}}{1}S=⟨I\left(R\right),J\left(S\right)⟩$$
23	11 22	syl5eqr	$$⊢\phi \to \underset{\dot{}}{1}\left(⟨R,S⟩\right)=⟨I\left(R\right),J\left(S\right)⟩$$