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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgru	⊢ Univ
1		vu	⊢ 𝑢
2	1	cv	⊢ 𝑢
3	2	wtr	⊢ Tr 𝑢
4		vx	⊢ 𝑥
5	4	cv	⊢ 𝑥
6	5	cpw	⊢ 𝒫 𝑥
7	6 2	wcel	⊢ 𝒫 𝑥 ∈ 𝑢
8		vy	⊢ 𝑦
9	8	cv	⊢ 𝑦
10	5 9	cpr	⊢ { 𝑥 , 𝑦 }
11	10 2	wcel	⊢ { 𝑥 , 𝑦 } ∈ 𝑢
12	11 8 2	wral	⊢ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢
13		cmap	⊢ ↑m
14	2 5 13	co	⊢ ( 𝑢 ↑m 𝑥 )
15	9	crn	⊢ ran 𝑦
16	15	cuni	⊢ ∪ ran 𝑦
17	16 2	wcel	⊢ ∪ ran 𝑦 ∈ 𝑢
18	17 8 14	wral	⊢ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢
19	7 12 18	w3a	⊢ ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 )
20	19 4 2	wral	⊢ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 )
21	3 20	wa	⊢ ( Tr 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) )
22	21 1	cab	⊢ { 𝑢 ∣ ( Tr 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ) }
23	0 22	wceq	⊢ Univ = { 𝑢 ∣ ( Tr 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ) }