Definition df-setc 15032

Description: Definition of the category Set, relativized to a subset u. This is the category of all sets in u and functions between these sets. Generally, we will take u to be a weak universe or Grothendieck universe, because these sets have closure properties as good as the real thing. (Contributed by FL, 8-Nov-2013.) (Revised by Mario Carneiro, 3-Jan-2017.)

Assertion

Ref	Expression
df-setc	|- SetCat = ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( y ^m x ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } )

Distinct variable group:   f, g, u, v, x, y, z

Detailed syntax breakdown of Definition df-setc

Step	Hyp	Ref	Expression
1		csetc 15031	. 2 class SetCat
2		vu	. . 3 setvar u
3		cvv 3054	. . 3 class _V
4		cnx 14259	. . . . . 6 class ndx
5		cbs 14262	. . . . . 6 class Base
6	4, 5	cfv 5502	. . . . 5 class ( Base ` ndx )
7	2	cv 1369	. . . . 5 class u
8	6, 7	cop 3967	. . . 4 class <. ( Base ` ndx ) , u >.
9		chom 14337	. . . . . 6 class Hom
10	4, 9	cfv 5502	. . . . 5 class ( Hom ` ndx )
11		vx	. . . . . 6 setvar x
12		vy	. . . . . 6 setvar y
13	12	cv 1369	. . . . . . 7 class y
14	11	cv 1369	. . . . . . 7 class x
15		cmap 7300	. . . . . . 7 class ^m
16	13, 14, 15	co 6176	. . . . . 6 class ( y ^m x )
17	11, 12, 7, 7, 16	cmpt2 6178	. . . . 5 class ( x e. u , y e. u |-> ( y ^m x ) )
18	10, 17	cop 3967	. . . 4 class <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( y ^m x ) ) >.
19		cco 14338	. . . . . 6 class comp
20	4, 19	cfv 5502	. . . . 5 class (comp ` ndx )
21		vv	. . . . . 6 setvar v
22		vz	. . . . . 6 setvar z
23	7, 7	cxp 4922	. . . . . 6 class ( u X. u )
24		vg	. . . . . . 7 setvar g
25		vf	. . . . . . 7 setvar f
26	22	cv 1369	. . . . . . . 8 class z
27	21	cv 1369	. . . . . . . . 9 class v
28		c2nd 6662	. . . . . . . . 9 class 2nd
29	27, 28	cfv 5502	. . . . . . . 8 class ( 2nd ` v )
30	26, 29, 15	co 6176	. . . . . . 7 class ( z ^m ( 2nd ` v ) )
31		c1st 6661	. . . . . . . . 9 class 1st
32	27, 31	cfv 5502	. . . . . . . 8 class ( 1st ` v )
33	29, 32, 15	co 6176	. . . . . . 7 class ( ( 2nd ` v ) ^m ( 1st ` v ) )
34	24	cv 1369	. . . . . . . 8 class g
35	25	cv 1369	. . . . . . . 8 class f
36	34, 35	ccom 4928	. . . . . . 7 class ( g o. f )
37	24, 25, 30, 33, 36	cmpt2 6178	. . . . . 6 class ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) )
38	21, 22, 23, 7, 37	cmpt2 6178	. . . . 5 class ( v e. ( u X. u ) , z e. u |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) )
39	20, 38	cop 3967	. . . 4 class <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >.
40	8, 18, 39	ctp 3965	. . 3 class { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( y ^m x ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. }
41	2, 3, 40	cmpt 4434	. 2 class ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( y ^m x ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } )
42	1, 41	wceq 1370	1 wff SetCat = ( u e. _V |-> { <. ( Base ` ndx ) , u >. , <. ( Hom ` ndx ) , ( x e. u , y e. u |-> ( y ^m x ) ) >. , <. (comp ` ndx ) , ( v e. ( u X. u ) , z e. u |-> ( g e. ( z ^m ( 2nd ` v ) ) , f e. ( ( 2nd ` v ) ^m ( 1st ` v ) ) |-> ( g o. f ) ) ) >. } )

This definition is referenced by:  setcval  15033