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

Metamath Proof Explorer

Theorem subccat

Description: A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subccat.1 ⊢ D = C ↾ cat J
subccat.j ⊢ φ → J ∈ Subcat ⁡ C
Assertion subccat ⊢ φ → D ∈ Cat

Proof

Step Hyp Ref Expression
1 subccat.1 ⊢ D = C ↾ cat J
2 subccat.j ⊢ φ → J ∈ Subcat ⁡ C
3 eqidd ⊢ φ → dom ⁡ dom ⁡ J = dom ⁡ dom ⁡ J
4 2 3 subcfn ⊢ φ → J Fn dom ⁡ dom ⁡ J × dom ⁡ dom ⁡ J
5 eqid ⊢ Id ⁡ C = Id ⁡ C
6 1 2 4 5 subccatid ⊢ φ → D ∈ Cat ∧ Id ⁡ D = x ∈ dom ⁡ dom ⁡ J ⟼ Id ⁡ C ⁡ x
7 6 simpld ⊢ φ → D ∈ Cat