This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 × c D
xpccat.c ⊢ φ → C ∈ Cat
xpccat.d ⊢ φ → D ∈ Cat
Assertion xpccat ⊢ φ → T ∈ Cat

Proof

Step Hyp Ref Expression
1 xpccat.t ⊢ T = C × c D
2 xpccat.c ⊢ φ → C ∈ Cat
3 xpccat.d ⊢ φ → D ∈ 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 ⊢ φ → T ∈ Cat ∧ Id ⁡ T = x ∈ Base C , y ∈ Base D ⟼ Id ⁡ C ⁡ x Id ⁡ D ⁡ y
9 8 simpld ⊢ φ → T ∈ Cat