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	|- C_cat = { <. h , j >. | E. t ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cssc	|- C_cat
1		vh	|- h
2		vj	|- j
3		vt	|- t
4	2	cv	|- j
5	3	cv	|- t
6	5 5	cxp	|- ( t X. t )
7	4 6	wfn	|- j Fn ( t X. t )
8		vs	|- s
9	5	cpw	|- ~P t
10	1	cv	|- h
11		vx	|- x
12	8	cv	|- s
13	12 12	cxp	|- ( s X. s )
14	11	cv	|- x
15	14 4	cfv	|- ( j ` x )
16	15	cpw	|- ~P ( j ` x )
17	11 13 16	cixp	|- X_ x e. ( s X. s ) ~P ( j ` x )
18	10 17	wcel	|- h e. X_ x e. ( s X. s ) ~P ( j ` x )
19	18 8 9	wrex	|- E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x )
20	7 19	wa	|- ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) )
21	20 3	wex	|- E. t ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) )
22	21 1 2	copab	|- { <. h , j >. | E. t ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) ) }
23	0 22	wceq	|- C_cat = { <. h , j >. | E. t ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) ) }