Definition df-gru 9613

Description: A Grothendieck universe is a set that is closed with respect to all the operations that are common in set theory: pairs, powersets, unions, intersections, Cartesian products etc. Grothendieck and alii, Séminaire de Géométrie Algébrique 4, Exposé I, p. 185. It was designed to give a precise meaning to the concepts of categories of sets, groups... (Contributed by Mario Carneiro, 9-Jun-2013.)

Assertion

Ref	Expression
df-gru	|- Univ = { u | ( Tr u /\ A. x e. u ( ~P x e. u /\ A. y e. u { x , y } e. u /\ A. y e. ( u ^m x ) U. ran y e. u ) ) }

Distinct variable group:   x, u, y

Detailed syntax breakdown of Definition df-gru

Step	Hyp	Ref	Expression
1		cgru 9612	. 2 class Univ
2		vu	. . . . . 6 setvar u
3	2	cv 1482	. . . . 5 class u
4	3	wtr 4752	. . . 4 wff Tr u
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1482	. . . . . . . 8 class x
7	6	cpw 4158	. . . . . . 7 class ~P x
8	7, 3	wcel 1990	. . . . . 6 wff ~P x e. u
9		vy	. . . . . . . . . 10 setvar y
10	9	cv 1482	. . . . . . . . 9 class y
11	6, 10	cpr 4179	. . . . . . . 8 class { x , y }
12	11, 3	wcel 1990	. . . . . . 7 wff { x , y } e. u
13	12, 9, 3	wral 2912	. . . . . 6 wff A. y e. u { x , y } e. u
14	10	crn 5115	. . . . . . . . 9 class ran y
15	14	cuni 4436	. . . . . . . 8 class U. ran y
16	15, 3	wcel 1990	. . . . . . 7 wff U. ran y e. u
17		cmap 7857	. . . . . . . 8 class ^m
18	3, 6, 17	co 6650	. . . . . . 7 class ( u ^m x )
19	16, 9, 18	wral 2912	. . . . . 6 wff A. y e. ( u ^m x ) U. ran y e. u
20	8, 13, 19	w3a 1037	. . . . 5 wff ( ~P x e. u /\ A. y e. u { x , y } e. u /\ A. y e. ( u ^m x ) U. ran y e. u )
21	20, 5, 3	wral 2912	. . . 4 wff A. x e. u ( ~P x e. u /\ A. y e. u { x , y } e. u /\ A. y e. ( u ^m x ) U. ran y e. u )
22	4, 21	wa 384	. . 3 wff ( Tr u /\ A. x e. u ( ~P x e. u /\ A. y e. u { x , y } e. u /\ A. y e. ( u ^m x ) U. ran y e. u ) )
23	22, 2	cab 2608	. 2 class { u | ( Tr u /\ A. x e. u ( ~P x e. u /\ A. y e. u { x , y } e. u /\ A. y e. ( u ^m x ) U. ran y e. u ) ) }
24	1, 23	wceq 1483	1 wff Univ = { u | ( Tr u /\ A. x e. u ( ~P x e. u /\ A. y e. u { x , y } e. u /\ A. y e. ( u ^m x ) U. ran y e. u ) ) }

This definition is referenced by:  elgrug  9614