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

Definition df-gru 8658
 Description: A Grothendieck's universe is a set that is closed with respect to all the operations that are common in set theory: pairs, powersets, unions, intersections, cross 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 8657 . 2
2 vu . . . . . 6
32cv 1651 . . . . 5
43wtr 4294 . . . 4
5 vx . . . . . . . . 9
65cv 1651 . . . . . . . 8
76cpw 3791 . . . . . . 7
87, 3wcel 1725 . . . . . 6
9 vy . . . . . . . . . 10
109cv 1651 . . . . . . . . 9
116, 10cpr 3807 . . . . . . . 8
1211, 3wcel 1725 . . . . . . 7
1312, 9, 3wral 2697 . . . . . 6
1410crn 4871 . . . . . . . . 9
1514cuni 4007 . . . . . . . 8
1615, 3wcel 1725 . . . . . . 7
17 cmap 7010 . . . . . . . 8
183, 6, 17co 6073 . . . . . . 7
1916, 9, 18wral 2697 . . . . . 6
208, 13, 19w3a 936 . . . . 5
2120, 5, 3wral 2697 . . . 4
224, 21wa 359 . . 3
2322, 2cab 2421 . 2
241, 23wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  elgrug  8659
 Copyright terms: Public domain W3C validator