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 ( 𝜑𝐽 ∈ ( Subcat ‘ 𝐶 ) )
subcssc.h 𝐻 = ( Homf𝐶 )
Assertion subcssc ( 𝜑𝐽cat 𝐻 )

Proof

Step Hyp Ref Expression
1 subcixp.1 ( 𝜑𝐽 ∈ ( Subcat ‘ 𝐶 ) )
2 subcssc.h 𝐻 = ( Homf𝐶 )
3 eqid ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
4 eqid ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
5 subcrcl ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat )
6 1 5 syl ( 𝜑𝐶 ∈ Cat )
7 eqidd ( 𝜑 → dom dom 𝐽 = dom dom 𝐽 )
8 2 3 4 6 7 issubc ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽cat 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐽 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ dom dom 𝐽𝑧 ∈ dom dom 𝐽𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
9 1 8 mpbid ( 𝜑 → ( 𝐽cat 𝐻 ∧ ∀ 𝑥 ∈ dom dom 𝐽 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ dom dom 𝐽𝑧 ∈ dom dom 𝐽𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
10 9 simpld ( 𝜑𝐽cat 𝐻 )