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 9716
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 9754) whereas the analogue for Grothendieck universes requires ax-groth 9837 (see grothtsk 9849). (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 9714 . 2 class WUni
2 vu . . . . . 6 setvar 𝑢
32cv 1631 . . . . 5 class 𝑢
43wtr 4904 . . . 4 wff Tr 𝑢
5 c0 4058 . . . . 5 class
63, 5wne 2932 . . . 4 wff 𝑢 ≠ ∅
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1631 . . . . . . . 8 class 𝑥
98cuni 4588 . . . . . . 7 class 𝑥
109, 3wcel 2139 . . . . . 6 wff 𝑥𝑢
118cpw 4302 . . . . . . 7 class 𝒫 𝑥
1211, 3wcel 2139 . . . . . 6 wff 𝒫 𝑥𝑢
13 vy . . . . . . . . . 10 setvar 𝑦
1413cv 1631 . . . . . . . . 9 class 𝑦
158, 14cpr 4323 . . . . . . . 8 class {𝑥, 𝑦}
1615, 3wcel 2139 . . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
1716, 13, 3wral 3050 . . . . . 6 wff 𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢
1810, 12, 17w3a 1072 . . . . 5 wff ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
1918, 7, 3wral 3050 . . . 4 wff 𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
204, 6, 19w3a 1072 . . 3 wff (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))
2120, 2cab 2746 . 2 class {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
221, 21wceq 1632 1 wff WUni = {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
Colors of variables: wff setvar class
This definition is referenced by:  iswun  9718
  Copyright terms: Public domain W3C validator