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 \land \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in 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 \in u$
8		vy	$setvar y$
9	8	cv	$setvar y$
10	5 9	cpr	$class \{x, y\}$
11	10 2	wcel	$wff \{x, y\} \in u$
12	11 8 2	wral	$wff \forall y \in u \{x, y\} \in 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 \in u$
18	17 8 14	wral	$wff \forall y \in (u^{x}) ⋃ ran y \in u$
19	7 12 18	w3a	$wff (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u)$
20	19 4 2	wral	$wff \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u)$
21	3 20	wa	$wff (Tr u \land \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u))$
22	21 1	cab	$class \{u \| (Tr u \land \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u))\}$
23	0 22	wceq	$wff Univ = \{u \| (Tr u \land \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u))\}$

Metamath Proof Explorer

Definition df-gru

Detailed syntax breakdown