Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gru Structured version   Unicode version

Definition df-gru 9205
 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-gru
StepHypRef Expression
1 cgru 9204 . 2
2 vu . . . . . 6
32cv 1436 . . . . 5
43wtr 4511 . . . 4
5 vx . . . . . . . . 9
65cv 1436 . . . . . . . 8
76cpw 3976 . . . . . . 7
87, 3wcel 1867 . . . . . 6
9 vy . . . . . . . . . 10
109cv 1436 . . . . . . . . 9
116, 10cpr 3995 . . . . . . . 8
1211, 3wcel 1867 . . . . . . 7
1312, 9, 3wral 2773 . . . . . 6
1410crn 4846 . . . . . . . . 9
1514cuni 4213 . . . . . . . 8
1615, 3wcel 1867 . . . . . . 7
17 cmap 7471 . . . . . . . 8
183, 6, 17co 6296 . . . . . . 7
1916, 9, 18wral 2773 . . . . . 6
208, 13, 19w3a 982 . . . . 5
2120, 5, 3wral 2773 . . . 4
224, 21wa 370 . . 3
2322, 2cab 2405 . 2
241, 23wceq 1437 1
 Colors of variables: wff setvar class This definition is referenced by:  elgrug  9206
 Copyright terms: Public domain W3C validator