# Metamath Proof Explorer

## 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 ${⊢}\mathrm{Univ}=\left\{{u}|\left(\mathrm{Tr}{u}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cgru ${class}\mathrm{Univ}$
1 vu ${setvar}{u}$
2 1 cv ${setvar}{u}$
3 2 wtr ${wff}\mathrm{Tr}{u}$
4 vx ${setvar}{x}$
5 4 cv ${setvar}{x}$
6 5 cpw ${class}𝒫{x}$
7 6 2 wcel ${wff}𝒫{x}\in {u}$
8 vy ${setvar}{y}$
9 8 cv ${setvar}{y}$
10 5 9 cpr ${class}\left\{{x},{y}\right\}$
11 10 2 wcel ${wff}\left\{{x},{y}\right\}\in {u}$
12 11 8 2 wral ${wff}\forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}$
13 cmap ${class}{↑}_{𝑚}$
14 2 5 13 co ${class}\left({{u}}^{{x}}\right)$
15 9 crn ${class}\mathrm{ran}{y}$
16 15 cuni ${class}\bigcup \mathrm{ran}{y}$
17 16 2 wcel ${wff}\bigcup \mathrm{ran}{y}\in {u}$
18 17 8 14 wral ${wff}\forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}$
19 7 12 18 w3a ${wff}\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)$
20 19 4 2 wral ${wff}\forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)$
21 3 20 wa ${wff}\left(\mathrm{Tr}{u}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)\right)$
22 21 1 cab ${class}\left\{{u}|\left(\mathrm{Tr}{u}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)\right)\right\}$
23 0 22 wceq ${wff}\mathrm{Univ}=\left\{{u}|\left(\mathrm{Tr}{u}\wedge \forall {x}\in {u}\phantom{\rule{.4em}{0ex}}\left(𝒫{x}\in {u}\wedge \forall {y}\in {u}\phantom{\rule{.4em}{0ex}}\left\{{x},{y}\right\}\in {u}\wedge \forall {y}\in \left({{u}}^{{x}}\right)\phantom{\rule{.4em}{0ex}}\bigcup \mathrm{ran}{y}\in {u}\right)\right)\right\}$