Definition df-gru

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgru	|- Univ
1		vu	|- u
2	1	cv	|- u
3	2	wtr	|- Tr u
4		vx	|- x
5	4	cv	|- x
6	5	cpw	|- ~P x
7	6 2	wcel	|- ~P x e. u
8		vy	|- y
9	8	cv	|- y
10	5 9	cpr	|- { x , y }
11	10 2	wcel	|- { x , y } e. u
12	11 8 2	wral	|- A. y e. u { x , y } e. u
13		cmap	|- ^m
14	2 5 13	co	|- ( u ^m x )
15	9	crn	|- ran y
16	15	cuni	|- U. ran y
17	16 2	wcel	|- U. ran y e. u
18	17 8 14	wral	|- A. y e. ( u ^m x ) U. ran y e. u
19	7 12 18	w3a	|- ( ~P x e. u /\ A. y e. u { x , y } e. u /\ A. y e. ( u ^m x ) U. ran y e. u )
20	19 4 2	wral	|- 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 )
21	3 20	wa	|- ( 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 ) )
22	21 1	cab	|- { 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 ) ) }
23	0 22	wceq	|- 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 ) ) }