Theorem ssc2

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

	Ref	Expression
Hypotheses	ssc2.1	|- ( ph -> H Fn ( S X. S ) )
	ssc2.2	|- ( ph -> H C_cat J )
	ssc2.3	|- ( ph -> X e. S )
	ssc2.4	|- ( ph -> Y e. S )
Assertion	ssc2	|- ( ph -> ( X H Y ) C_ ( X J Y ) )

Proof

Step	Hyp	Ref	Expression
1		ssc2.1	|- ( ph -> H Fn ( S X. S ) )
2		ssc2.2	|- ( ph -> H C_cat J )
3		ssc2.3	|- ( ph -> X e. S )
4		ssc2.4	|- ( ph -> Y e. S )
5		eqidd	|- ( ph -> dom dom J = dom dom J )
6	2 5	sscfn2	|- ( ph -> J Fn ( dom dom J X. dom dom J ) )
7		sscrel	|- Rel C_cat
8	7	brrelex2i	|- ( H C_cat J -> J e. _V )
9		dmexg	|- ( J e. _V -> dom J e. _V )
10		dmexg	|- ( dom J e. _V -> dom dom J e. _V )
11	2 8 9 10	4syl	|- ( ph -> dom dom J e. _V )
12	1 6 11	isssc	|- ( ph -> ( H C_cat J <-> ( S C_ dom dom J /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) ) )
13	2 12	mpbid	|- ( ph -> ( S C_ dom dom J /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) )
14	13	simprd	|- ( ph -> A. x e. S A. y e. S ( x H y ) C_ ( x J y ) )
15		oveq1	|- ( x = X -> ( x H y ) = ( X H y ) )
16		oveq1	|- ( x = X -> ( x J y ) = ( X J y ) )
17	15 16	sseq12d	|- ( x = X -> ( ( x H y ) C_ ( x J y ) <-> ( X H y ) C_ ( X J y ) ) )
18		oveq2	|- ( y = Y -> ( X H y ) = ( X H Y ) )
19		oveq2	|- ( y = Y -> ( X J y ) = ( X J Y ) )
20	18 19	sseq12d	|- ( y = Y -> ( ( X H y ) C_ ( X J y ) <-> ( X H Y ) C_ ( X J Y ) ) )
21	17 20	rspc2va	|- ( ( ( X e. S /\ Y e. S ) /\ A. x e. S A. y e. S ( x H y ) C_ ( x J y ) ) -> ( X H Y ) C_ ( X J Y ) )
22	3 4 14 21	syl21anc	|- ( ph -> ( X H Y ) C_ ( X J Y ) )