Theorem subcss1

Description: The objects of a subcategory are a subset of the objects of the original. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	subcss1.1	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
	subcss1.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
	subcss1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	subcss1	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		subcss1.1	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
2		subcss1.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
3		subcss1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
5	4 3	homffn	⊢ ( Homf ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 )
6	5	a1i	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) )
7	1 4	subcssc	⊢ ( 𝜑 → 𝐽 ⊆cat ( Homf ‘ 𝐶 ) )
8	2 6 7	ssc1	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )