Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gru Structured version   Visualization version   GIF version

Definition df-gru 10205
 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
StepHypRef Expression
1 cgru 10204 . 2 class Univ
2 vu . . . . . 6 setvar 𝑢
32cv 1529 . . . . 5 class 𝑢
43wtr 5168 . . . 4 wff Tr 𝑢
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1529 . . . . . . . 8 class 𝑥
76cpw 4541 . . . . . . 7 class 𝒫 𝑥
87, 3wcel 2106 . . . . . 6 wff 𝒫 𝑥𝑢
9 vy . . . . . . . . . 10 setvar 𝑦
109cv 1529 . . . . . . . . 9 class 𝑦
116, 10cpr 4565 . . . . . . . 8 class {𝑥, 𝑦}
1211, 3wcel 2106 . . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
1312, 9, 3wral 3142 . . . . . 6 wff 𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢
1410crn 5554 . . . . . . . . 9 class ran 𝑦
1514cuni 4836 . . . . . . . 8 class ran 𝑦
1615, 3wcel 2106 . . . . . . 7 wff ran 𝑦𝑢
17 cmap 8399 . . . . . . . 8 class m
183, 6, 17co 7151 . . . . . . 7 class (𝑢m 𝑥)
1916, 9, 18wral 3142 . . . . . 6 wff 𝑦 ∈ (𝑢m 𝑥) ran 𝑦𝑢
208, 13, 19w3a 1081 . . . . 5 wff (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢m 𝑥) ran 𝑦𝑢)
2120, 5, 3wral 3142 . . . 4 wff 𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢m 𝑥) ran 𝑦𝑢)
224, 21wa 396 . . 3 wff (Tr 𝑢 ∧ ∀𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢m 𝑥) ran 𝑦𝑢))
2322, 2cab 2802 . 2 class {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢m 𝑥) ran 𝑦𝑢))}
241, 23wceq 1530 1 wff Univ = {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢m 𝑥) ran 𝑦𝑢))}
 Colors of variables: wff setvar class This definition is referenced by:  elgrug  10206
 Copyright terms: Public domain W3C validator