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

Definition df-wun 9730
Description: The class of all weak universes. A weak universe is a nonempty transitive class closed under union, pairing, and powerset. The advantage of weak universes over Grothendieck universes is that one can prove that every set is contained in a weak universe in ZF (see uniwun 9768) whereas the analogue for Grothendieck universes requires ax-groth 9851 (see grothtsk 9863). (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-wun WUni = {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
Distinct variable group:   𝑥,𝑦,𝑢

Detailed syntax breakdown of Definition df-wun
StepHypRef Expression
1 cwun 9728 . 2 class WUni
2 vu . . . . . 6 setvar 𝑢
32cv 1630 . . . . 5 class 𝑢
43wtr 4887 . . . 4 wff Tr 𝑢
5 c0 4063 . . . . 5 class
63, 5wne 2943 . . . 4 wff 𝑢 ≠ ∅
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1630 . . . . . . . 8 class 𝑥
98cuni 4575 . . . . . . 7 class 𝑥
109, 3wcel 2145 . . . . . 6 wff 𝑥𝑢
118cpw 4298 . . . . . . 7 class 𝒫 𝑥
1211, 3wcel 2145 . . . . . 6 wff 𝒫 𝑥𝑢
13 vy . . . . . . . . . 10 setvar 𝑦
1413cv 1630 . . . . . . . . 9 class 𝑦
158, 14cpr 4319 . . . . . . . 8 class {𝑥, 𝑦}
1615, 3wcel 2145 . . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
1716, 13, 3wral 3061 . . . . . 6 wff 𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢
1810, 12, 17w3a 1071 . . . . 5 wff ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
1918, 7, 3wral 3061 . . . 4 wff 𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
204, 6, 19w3a 1071 . . 3 wff (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))
2120, 2cab 2757 . 2 class {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
221, 21wceq 1631 1 wff WUni = {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
Colors of variables: wff setvar class
This definition is referenced by:  iswun  9732
  Copyright terms: Public domain W3C validator