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

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 𝐻 )