Definition df-gru 9613

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	⊢ Univ = {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑𝑚 𝑥)∪ ran 𝑦 ∈ 𝑢))}

Distinct variable group:   𝑥,𝑢,𝑦

Detailed syntax breakdown of Definition df-gru

Step	Hyp	Ref	Expression
1		cgru 9612	. 2 class Univ
2		vu	. . . . . 6 setvar 𝑢
3	2	cv 1482	. . . . 5 class 𝑢
4	3	wtr 4752	. . . 4 wff Tr 𝑢
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1482	. . . . . . . 8 class 𝑥
7	6	cpw 4158	. . . . . . 7 class 𝒫 𝑥
8	7, 3	wcel 1990	. . . . . 6 wff 𝒫 𝑥 ∈ 𝑢
9		vy	. . . . . . . . . 10 setvar 𝑦
10	9	cv 1482	. . . . . . . . 9 class 𝑦
11	6, 10	cpr 4179	. . . . . . . 8 class {𝑥, 𝑦}
12	11, 3	wcel 1990	. . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
13	12, 9, 3	wral 2912	. . . . . 6 wff ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢
14	10	crn 5115	. . . . . . . . 9 class ran 𝑦
15	14	cuni 4436	. . . . . . . 8 class ∪ ran 𝑦
16	15, 3	wcel 1990	. . . . . . 7 wff ∪ ran 𝑦 ∈ 𝑢
17		cmap 7857	. . . . . . . 8 class ↑𝑚
18	3, 6, 17	co 6650	. . . . . . 7 class (𝑢 ↑𝑚 𝑥)
19	16, 9, 18	wral 2912	. . . . . 6 wff ∀𝑦 ∈ (𝑢 ↑𝑚 𝑥)∪ ran 𝑦 ∈ 𝑢
20	8, 13, 19	w3a 1037	. . . . 5 wff (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑𝑚 𝑥)∪ ran 𝑦 ∈ 𝑢)
21	20, 5, 3	wral 2912	. . . 4 wff ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑𝑚 𝑥)∪ ran 𝑦 ∈ 𝑢)
22	4, 21	wa 384	. . 3 wff (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑𝑚 𝑥)∪ ran 𝑦 ∈ 𝑢))
23	22, 2	cab 2608	. 2 class {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑𝑚 𝑥)∪ ran 𝑦 ∈ 𝑢))}
24	1, 23	wceq 1483	1 wff Univ = {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑𝑚 𝑥)∪ ran 𝑦 ∈ 𝑢))}

This definition is referenced by:  elgrug  9614