Definition df-ssc 16470

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 16472, 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.)

Assertion

Ref	Expression
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 ) ) }

Distinct variable group:   h, j, s, t, x

Detailed syntax breakdown of Definition df-ssc

Step	Hyp	Ref	Expression
1		cssc 16467	. 2 class C_cat
2		vj	. . . . . . 7 setvar j
3	2	cv 1482	. . . . . 6 class j
4		vt	. . . . . . . 8 setvar t
5	4	cv 1482	. . . . . . 7 class t
6	5, 5	cxp 5112	. . . . . 6 class ( t X. t )
7	3, 6	wfn 5883	. . . . 5 wff j Fn ( t X. t )
8		vh	. . . . . . . 8 setvar h
9	8	cv 1482	. . . . . . 7 class h
10		vx	. . . . . . . 8 setvar x
11		vs	. . . . . . . . . 10 setvar s
12	11	cv 1482	. . . . . . . . 9 class s
13	12, 12	cxp 5112	. . . . . . . 8 class ( s X. s )
14	10	cv 1482	. . . . . . . . . 10 class x
15	14, 3	cfv 5888	. . . . . . . . 9 class ( j ` x )
16	15	cpw 4158	. . . . . . . 8 class ~P ( j ` x )
17	10, 13, 16	cixp 7908	. . . . . . 7 class X_ x e. ( s X. s ) ~P ( j ` x )
18	9, 17	wcel 1990	. . . . . 6 wff h e. X_ x e. ( s X. s ) ~P ( j ` x )
19	5	cpw 4158	. . . . . 6 class ~P t
20	18, 11, 19	wrex 2913	. . . . 5 wff E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x )
21	7, 20	wa 384	. . . 4 wff ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) )
22	21, 4	wex 1704	. . 3 wff E. t ( j Fn ( t X. t ) /\ E. s e. ~P t h e. X_ x e. ( s X. s ) ~P ( j ` x ) )
23	22, 8, 2	copab 4712	. 2 class { <. 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 ) ) }
24	1, 23	wceq 1483	1 wff 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 ) ) }

This definition is referenced by:  sscrel  16473  brssc  16474