Theorem ssc1

Description: Infer subset relation on objects from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	isssc.1	|- ( ph -> H Fn ( S X. S ) )
	isssc.2	|- ( ph -> J Fn ( T X. T ) )
	ssc1.3	|- ( ph -> H C_cat J )
Assertion	ssc1	|- ( ph -> S C_ T )

Proof

Step	Hyp	Ref	Expression
1		isssc.1	|- ( ph -> H Fn ( S X. S ) )
2		isssc.2	|- ( ph -> J Fn ( T X. T ) )
3		ssc1.3	|- ( ph -> H C_cat J )
4		sscrel	|- Rel C_cat
5	4	brrelex2i	|- ( H C_cat J -> J e. _V )
6	3 5	syl	|- ( ph -> J e. _V )
7	2	ssclem	|- ( ph -> ( J e. _V <-> T e. _V ) )
8	6 7	mpbid	|- ( ph -> T e. _V )
9	1 2 8	isssc	|- ( ph -> ( H C_cat J <-> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) )
10	3 9	mpbid	|- ( ph -> ( S C_ T /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) )
11	10	simpld	|- ( ph -> S C_ T )