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

Definition df-gru 9190
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 9189 . 2
2 vu . . . . . 6
32cv 1394 . . . . 5
43wtr 4545 . . . 4
5 vx . . . . . . . . 9
65cv 1394 . . . . . . . 8
76cpw 4012 . . . . . . 7
87, 3wcel 1818 . . . . . 6
9 vy . . . . . . . . . 10
109cv 1394 . . . . . . . . 9
116, 10cpr 4031 . . . . . . . 8
1211, 3wcel 1818 . . . . . . 7
1312, 9, 3wral 2807 . . . . . 6
1410crn 5005 . . . . . . . . 9
1514cuni 4249 . . . . . . . 8
1615, 3wcel 1818 . . . . . . 7
17 cmap 7439 . . . . . . . 8
183, 6, 17co 6296 . . . . . . 7
1916, 9, 18wral 2807 . . . . . 6
208, 13, 19w3a 973 . . . . 5
2120, 5, 3wral 2807 . . . 4
224, 21wa 369 . . 3
2322, 2cab 2442 . 2
241, 23wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  elgrug  9191
  Copyright terms: Public domain W3C validator