Definition df-gru 10876

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 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))}

Distinct variable group:   𝑥,𝑢,𝑦

Detailed syntax breakdown of Definition df-gru

Step	Hyp	Ref	Expression
1		cgru 10875	. 2 class Univ
2		vu	. . . . . 6 setvar 𝑢
3	2	cv 1569	. . . . 5 class 𝑢
4	3	wtr 5212	. . . 4 wff Tr 𝑢
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1569	. . . . . . . 8 class 𝑥
7	6	cpw 4557	. . . . . . 7 class 𝒫 𝑥
8	7, 3	wcel 2145	. . . . . 6 wff 𝒫 𝑥 ∈ 𝑢
9		vy	. . . . . . . . . 10 setvar 𝑦
10	9	cv 1569	. . . . . . . . 9 class 𝑦
11	6, 10	cpr 4586	. . . . . . . 8 class {𝑥, 𝑦}
12	11, 3	wcel 2145	. . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
13	12, 9, 3	wral 3077	. . . . . 6 wff ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢
14	10	crn 5652	. . . . . . . . 9 class ran 𝑦
15	14	cuni 4867	. . . . . . . 8 class ∪ ran 𝑦
16	15, 3	wcel 2145	. . . . . . 7 wff ∪ ran 𝑦 ∈ 𝑢
17		cmap 8847	. . . . . . . 8 class ↑m
18	3, 6, 17	co 7420	. . . . . . 7 class (𝑢 ↑m 𝑥)
19	16, 9, 18	wral 3077	. . . . . 6 wff ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢
20	8, 13, 19	w3a 1103	. . . . 5 wff (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢)
21	20, 5, 3	wral 3077	. . . 4 wff ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢)
22	4, 21	wa 401	. . 3 wff (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))
23	22, 2	cab 2739	. 2 class {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))}
24	1, 23	wceq 1570	1 wff Univ = {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥 ∈ 𝑢 (𝒫 𝑥 ∈ 𝑢 ∧ ∀𝑦 ∈ 𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢 ↑m 𝑥)∪ ran 𝑦 ∈ 𝑢))}

This definition is used by:  elgrug  10877