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	$$⊢\phi \to HFn\left(S\times S\right)$$
	isssc.2	$$⊢\phi \to JFn\left(T\times T\right)$$
	ssc1.3	$$⊢\phi \to H{\subseteq }_{\mathrm{cat}}J$$
Assertion	ssc1	$$⊢\phi \to S\subseteq T$$

Proof

Step	Hyp	Ref	Expression
1		isssc.1	$$⊢\phi \to HFn\left(S\times S\right)$$
2		isssc.2	$$⊢\phi \to JFn\left(T\times T\right)$$
3		ssc1.3	$$⊢\phi \to H{\subseteq }_{\mathrm{cat}}J$$
4		sscrel	$$⊢\mathrm{Rel}{\subseteq }_{\mathrm{cat}}$$
5	4	brrelex2i	$$⊢H{\subseteq }_{\mathrm{cat}}J\to J\in \mathrm{V}$$
6	3 5	syl	$$⊢\phi \to J\in \mathrm{V}$$
7	2	ssclem	$$⊢\phi \to \left(J\in \mathrm{V}\leftrightarrow T\in \mathrm{V}\right)$$
8	6 7	mpbid	$$⊢\phi \to T\in \mathrm{V}$$
9	1 2 8	isssc	$$⊢\phi \to \left(H{\subseteq }_{\mathrm{cat}}J\leftrightarrow \left(S\subseteq T\wedge \forall x\in S\forall y\in SxHy\subseteq xJy\right)\right)$$
10	3 9	mpbid	$$⊢\phi \to \left(S\subseteq T\wedge \forall x\in S\forall y\in SxHy\subseteq xJy\right)$$
11	10	simpld	$$⊢\phi \to S\subseteq T$$