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