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	$$⊢\phi \to HFn\left(S\times S\right)$$
	ssc2.2	$$⊢\phi \to H{\subseteq }_{\mathrm{cat}}J$$
	ssc2.3	$$⊢\phi \to X\in S$$
	ssc2.4	$$⊢\phi \to Y\in S$$
Assertion	ssc2	$$⊢\phi \to XHY\subseteq XJY$$

Proof

Step	Hyp	Ref	Expression
1		ssc2.1	$$⊢\phi \to HFn\left(S\times S\right)$$
2		ssc2.2	$$⊢\phi \to H{\subseteq }_{\mathrm{cat}}J$$
3		ssc2.3	$$⊢\phi \to X\in S$$
4		ssc2.4	$$⊢\phi \to Y\in S$$
5		eqidd	$$⊢\phi \to \mathrm{dom}\mathrm{dom}J=\mathrm{dom}\mathrm{dom}J$$
6	2 5	sscfn2	$$⊢\phi \to JFn\left(\mathrm{dom}\mathrm{dom}J\times \mathrm{dom}\mathrm{dom}J\right)$$
7		sscrel	$$⊢\mathrm{Rel}{\subseteq }_{\mathrm{cat}}$$
8	7	brrelex2i	$$⊢H{\subseteq }_{\mathrm{cat}}J\to J\in \mathrm{V}$$
9		dmexg	$$⊢J\in \mathrm{V}\to \mathrm{dom}J\in \mathrm{V}$$
10		dmexg	$$⊢\mathrm{dom}J\in \mathrm{V}\to \mathrm{dom}\mathrm{dom}J\in \mathrm{V}$$
11	2 8 9 10	4syl	$$⊢\phi \to \mathrm{dom}\mathrm{dom}J\in \mathrm{V}$$
12	1 6 11	isssc	$$⊢\phi \to \left(H{\subseteq }_{\mathrm{cat}}J\leftrightarrow \left(S\subseteq \mathrm{dom}\mathrm{dom}J\wedge \forall x\in S\forall y\in SxHy\subseteq xJy\right)\right)$$
13	2 12	mpbid	$$⊢\phi \to \left(S\subseteq \mathrm{dom}\mathrm{dom}J\wedge \forall x\in S\forall y\in SxHy\subseteq xJy\right)$$
14	13	simprd	$$⊢\phi \to \forall x\in S\forall y\in SxHy\subseteq xJy$$
15		oveq1	$$⊢x=X\to xHy=XHy$$
16		oveq1	$$⊢x=X\to xJy=XJy$$
17	15 16	sseq12d	$$⊢x=X\to \left(xHy\subseteq xJy\leftrightarrow XHy\subseteq XJy\right)$$
18		oveq2	$$⊢y=Y\to XHy=XHY$$
19		oveq2	$$⊢y=Y\to XJy=XJY$$
20	18 19	sseq12d	$$⊢y=Y\to \left(XHy\subseteq XJy\leftrightarrow XHY\subseteq XJY\right)$$
21	17 20	rspc2va	$$⊢\left(\left(X\in S\wedge Y\in S\right)\wedge \forall x\in S\forall y\in SxHy\subseteq xJy\right)\to XHY\subseteq XJY$$
22	3 4 14 21	syl21anc	$$⊢\phi \to XHY\subseteq XJY$$