Theorem sscrel

Description: The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Assertion	sscrel	$$⊢\mathrm{Rel}{\subseteq }_{\mathrm{cat}}$$

Proof

Step	Hyp	Ref	Expression
1		df-ssc	$$⊢{\subseteq }_{\mathrm{cat}}=\left\{⟨h,j⟩|\exists t\left(jFn\left(t\times t\right)\wedge \exists s\in 𝒫th\in \underset{x\in s\times s}{⨉}𝒫j\left(x\right)\right)\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}{\subseteq }_{\mathrm{cat}}$$