Theorem subcss2

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

	Ref	Expression
Hypotheses	subcss1.1	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
	subcss1.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
	subcss2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	subcss2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	subcss2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion	subcss2	⊢ ( 𝜑 → ( 𝑋 𝐽 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		subcss1.1	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
2		subcss1.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
3		subcss2.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		subcss2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
5		subcss2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
6		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
7	1 6	subcssc	⊢ ( 𝜑 → 𝐽 ⊆cat ( Homf ‘ 𝐶 ) )
8	2 7 4 5	ssc2	⊢ ( 𝜑 → ( 𝑋 𝐽 𝑌 ) ⊆ ( 𝑋 ( Homf ‘ 𝐶 ) 𝑌 ) )
9		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
10	1 2 9	subcss1	⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
11	10 4	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
12	10 5	sseldd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
13	6 9 3 11 12	homfval	⊢ ( 𝜑 → ( 𝑋 ( Homf ‘ 𝐶 ) 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )
14	8 13	sseqtrd	⊢ ( 𝜑 → ( 𝑋 𝐽 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )