Metamath Proof Explorer

Theorem subcssc

Description: An element in the set of subcategories is a subset of the category. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses subcixp.1 ⊢ φ → J ∈ Subcat ⁡ C
subcssc.h ⊢ H = Hom 𝑓 ⁡ C
Assertion subcssc ⊢ φ → J ⊆ cat H

Proof

Step Hyp Ref Expression
1 subcixp.1 ⊢ φ → J ∈ Subcat ⁡ C
2 subcssc.h ⊢ H = Hom 𝑓 ⁡ C
3 eqid ⊢ Id ⁡ C = Id ⁡ C
4 eqid ⊢ comp ⁡ C = comp ⁡ C
5 subcrcl ⊢ J ∈ Subcat ⁡ C → C ∈ Cat
6 1 5 syl ⊢ φ → C ∈ Cat
7 eqidd ⊢ φ → dom ⁡ dom ⁡ J = dom ⁡ dom ⁡ J
8 2 3 4 6 7 issubc ⊢ φ → J ∈ Subcat ⁡ C ↔ J ⊆ cat H ∧ ∀ x ∈ dom ⁡ dom ⁡ J Id ⁡ C ⁡ x ∈ x J x ∧ ∀ y ∈ dom ⁡ dom ⁡ J ∀ z ∈ dom ⁡ dom ⁡ J ∀ f ∈ x J y ∀ g ∈ y J z g x y comp ⁡ C z f ∈ x J z
9 1 8 mpbid ⊢ φ → J ⊆ cat H ∧ ∀ x ∈ dom ⁡ dom ⁡ J Id ⁡ C ⁡ x ∈ x J x ∧ ∀ y ∈ dom ⁡ dom ⁡ J ∀ z ∈ dom ⁡ dom ⁡ J ∀ f ∈ x J y ∀ g ∈ y J z g x y comp ⁡ C z f ∈ x J z
10 9 simpld ⊢ φ → J ⊆ cat H