Description: A subcategory is a category. (Contributed by Mario Carneiro, 4-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subccat.1 | ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 ) | |
subccat.j | ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) | ||
Assertion | subccat | ⊢ ( 𝜑 → 𝐷 ∈ Cat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subccat.1 | ⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 ) | |
2 | subccat.j | ⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) | |
3 | eqidd | ⊢ ( 𝜑 → dom dom 𝐽 = dom dom 𝐽 ) | |
4 | 2 3 | subcfn | ⊢ ( 𝜑 → 𝐽 Fn ( dom dom 𝐽 × dom dom 𝐽 ) ) |
5 | eqid | ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 ) | |
6 | 1 2 4 5 | subccatid | ⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ ( Id ‘ 𝐷 ) = ( 𝑥 ∈ dom dom 𝐽 ↦ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) ) ) |
7 | 6 | simpld | ⊢ ( 𝜑 → 𝐷 ∈ Cat ) |