Definition df-ssc

Description: Define the subset relation for subcategories. Despite the name, this is not really a "category-aware" definition, which is to say it makes no explicit references to homsets or composition; instead this is a subset-like relation on the functions that are used as subcategory specifications in df-subc , which makes it play an analogous role to the subset relation applied to the subgroups of a group. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Assertion	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\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cssc	$$class{\subseteq }_{\mathrm{cat}}$$
1		vh	$$setvarh$$
2		vj	$$setvarj$$
3		vt	$$setvart$$
4	2	cv	$$setvarj$$
5	3	cv	$$setvart$$
6	5 5	cxp	$$class\left(t\times t\right)$$
7	4 6	wfn	$$wffjFn\left(t\times t\right)$$
8		vs	$$setvars$$
9	5	cpw	$$class𝒫t$$
10	1	cv	$$setvarh$$
11		vx	$$setvarx$$
12	8	cv	$$setvars$$
13	12 12	cxp	$$class\left(s\times s\right)$$
14	11	cv	$$setvarx$$
15	14 4	cfv	$$classj\left(x\right)$$
16	15	cpw	$$class𝒫j\left(x\right)$$
17	11 13 16	cixp	$$class\underset{x\in s\times s}{⨉}𝒫j\left(x\right)$$
18	10 17	wcel	$$wffh\in \underset{x\in s\times s}{⨉}𝒫j\left(x\right)$$
19	18 8 9	wrex	$$wff\exists s\in 𝒫th\in \underset{x\in s\times s}{⨉}𝒫j\left(x\right)$$
20	7 19	wa	$$wff\left(jFn\left(t\times t\right)\wedge \exists s\in 𝒫th\in \underset{x\in s\times s}{⨉}𝒫j\left(x\right)\right)$$
21	20 3	wex	$$wff\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)$$
22	21 1 2	copab	$$class\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\}$$
23	0 22	wceq	$$wff{\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\}$$