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 Xc. D )
	xpccat.c	|- ( ph -> C e. Cat )
	xpccat.d	|- ( ph -> D e. Cat )
Assertion	xpccat	|- ( ph -> T e. Cat )

Proof

Step	Hyp	Ref	Expression
1		xpccat.t	|- T = ( C Xc. D )
2		xpccat.c	|- ( ph -> C e. Cat )
3		xpccat.d	|- ( ph -> D e. Cat )
4		eqid	|- ( Base ` C ) = ( Base ` C )
5		eqid	|- ( Base ` D ) = ( Base ` D )
6		eqid	|- ( Id ` C ) = ( Id ` C )
7		eqid	|- ( Id ` D ) = ( Id ` D )
8	1 2 3 4 5 6 7	xpccatid	|- ( ph -> ( T e. Cat /\ ( Id ` T ) = ( x e. ( Base ` C ) , y e. ( Base ` D ) |-> <. ( ( Id ` C ) ` x ) , ( ( Id ` D ) ` y ) >. ) ) )
9	8	simpld	|- ( ph -> T e. Cat )