Theorem xpccat

Description: The product of two categories is a category. (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}$$
Assertion	xpccat	$$⊢\phi \to T\in \mathrm{Cat}$$

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		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
5		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
6		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
7		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
8	1 2 3 4 5 6 7	xpccatid	$$⊢\phi \to \left(T\in \mathrm{Cat}\wedge \mathrm{Id}\left(T\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_D⟼⟨\mathrm{Id}\left(C\right)\left(x\right),\mathrm{Id}\left(D\right)\left(y\right)⟩\right)\right)$$
9	8	simpld	$$⊢\phi \to T\in \mathrm{Cat}$$