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 ⊢ Univ = u | Tr ⁡ u ∧ ∀ x ∈ u 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgru class Univ
1 vu setvar u
2 1 cv setvar u
3 2 wtr wff Tr ⁡ u
4 vx setvar x
5 4 cv setvar x
6 5 cpw class 𝒫 x
7 6 2 wcel wff 𝒫 x ∈ u
8 vy setvar y
9 8 cv setvar y
10 5 9 cpr class x y
11 10 2 wcel wff x y ∈ u
12 11 8 2 wral wff ∀ y ∈ u x y ∈ u
13 cmap class ↑ 𝑚
14 2 5 13 co class u x
15 9 crn class ran ⁡ y
16 15 cuni class ⋃ ran ⁡ y
17 16 2 wcel wff ⋃ ran ⁡ y ∈ u
18 17 8 14 wral wff ∀ y ∈ u x ⋃ ran ⁡ y ∈ u
19 7 12 18 w3a wff 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u
20 19 4 2 wral wff ∀ x ∈ u 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u
21 3 20 wa wff Tr ⁡ u ∧ ∀ x ∈ u 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u
22 21 1 cab class u | Tr ⁡ u ∧ ∀ x ∈ u 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u
23 0 22 wceq wff Univ = u | Tr ⁡ u ∧ ∀ x ∈ u 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u ∧ ∀ y ∈ u x ⋃ ran ⁡ y ∈ u