Theorem xpccat

Description: The product of two categories is a category. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	xpccat.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	xpccat.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	xpccat.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	xpccat	⊢ ( 𝜑 → 𝑇 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		xpccat.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		xpccat.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		xpccat.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
7		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
8	1 2 3 4 5 6 7	xpccatid	⊢ ( 𝜑 → ( 𝑇 ∈ Cat ∧ ( Id ‘ 𝑇 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ⟨ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) , ( ( Id ‘ 𝐷 ) ‘ 𝑦 ) ⟩ ) ) )
9	8	simpld	⊢ ( 𝜑 → 𝑇 ∈ Cat )