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

Definition df-gru 9469
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 9468 . 2 class Univ
2 vu . . . . . 6 setvar 𝑢
32cv 1473 . . . . 5 class 𝑢
43wtr 4674 . . . 4 wff Tr 𝑢
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1473 . . . . . . . 8 class 𝑥
76cpw 4107 . . . . . . 7 class 𝒫 𝑥
87, 3wcel 1976 . . . . . 6 wff 𝒫 𝑥𝑢
9 vy . . . . . . . . . 10 setvar 𝑦
109cv 1473 . . . . . . . . 9 class 𝑦
116, 10cpr 4126 . . . . . . . 8 class {𝑥, 𝑦}
1211, 3wcel 1976 . . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
1312, 9, 3wral 2895 . . . . . 6 wff 𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢
1410crn 5029 . . . . . . . . 9 class ran 𝑦
1514cuni 4366 . . . . . . . 8 class ran 𝑦
1615, 3wcel 1976 . . . . . . 7 wff ran 𝑦𝑢
17 cmap 7721 . . . . . . . 8 class 𝑚
183, 6, 17co 6527 . . . . . . 7 class (𝑢𝑚 𝑥)
1916, 9, 18wral 2895 . . . . . 6 wff 𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢
208, 13, 19w3a 1030 . . . . 5 wff (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢)
2120, 5, 3wral 2895 . . . 4 wff 𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢)
224, 21wa 382 . . 3 wff (Tr 𝑢 ∧ ∀𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢))
2322, 2cab 2595 . 2 class {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢))}
241, 23wceq 1474 1 wff Univ = {𝑢 ∣ (Tr 𝑢 ∧ ∀𝑥𝑢 (𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢 ∧ ∀𝑦 ∈ (𝑢𝑚 𝑥) ran 𝑦𝑢))}
Colors of variables: wff setvar class
This definition is referenced by:  elgrug  9470
  Copyright terms: Public domain W3C validator