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

Definition df-gru 9651
 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
StepHypRef Expression
1 cgru 9650 . 2 class Univ
2 vu . . . . . 6 setvar 𝑢
32cv 1522 . . . . 5 class 𝑢
43wtr 4785 . . . 4 wff Tr 𝑢
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1522 . . . . . . . 8 class 𝑥
76cpw 4191 . . . . . . 7 class 𝒫 𝑥
87, 3wcel 2030 . . . . . 6 wff 𝒫 𝑥𝑢
9 vy . . . . . . . . . 10 setvar 𝑦
109cv 1522 . . . . . . . . 9 class 𝑦
116, 10cpr 4212 . . . . . . . 8 class {𝑥, 𝑦}
1211, 3wcel 2030 . . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
1312, 9, 3wral 2941 . . . . . 6 wff 𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢
1410crn 5144 . . . . . . . . 9 class ran 𝑦
1514cuni 4468 . . . . . . . 8 class ran 𝑦
1615, 3wcel 2030 . . . . . . 7 wff ran 𝑦𝑢
17 cmap 7899 . . . . . . . 8 class 𝑚
183, 6, 17co 6690 . . . . . . 7 class (𝑢𝑚 𝑥)
1916, 9, 18wral 2941 . . . . . 6 wff 𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢
208, 13, 19w3a 1054 . . . . 5 wff (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢)
2120, 5, 3wral 2941 . . . 4 wff 𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢)
224, 21wa 383 . . 3 wff (Tr 𝑢 ∧ ∀𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢))
2322, 2cab 2637 . 2 class {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢))}
241, 23wceq 1523 1 wff Univ = {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢))}
 Colors of variables: wff setvar class This definition is referenced by:  elgrug  9652
 Copyright terms: Public domain W3C validator