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 10113
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 10151) whereas the analogue for Grothendieck universes requires ax-groth 10234 (see grothtsk 10246). (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 10111 . 2 class WUni
2 vu . . . . . 6 setvar 𝑢
32cv 1527 . . . . 5 class 𝑢
43wtr 5164 . . . 4 wff Tr 𝑢
5 c0 4290 . . . . 5 class
63, 5wne 3016 . . . 4 wff 𝑢 ≠ ∅
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1527 . . . . . . . 8 class 𝑥
98cuni 4832 . . . . . . 7 class 𝑥
109, 3wcel 2105 . . . . . 6 wff 𝑥𝑢
118cpw 4537 . . . . . . 7 class 𝒫 𝑥
1211, 3wcel 2105 . . . . . 6 wff 𝒫 𝑥𝑢
13 vy . . . . . . . . . 10 setvar 𝑦
1413cv 1527 . . . . . . . . 9 class 𝑦
158, 14cpr 4561 . . . . . . . 8 class {𝑥, 𝑦}
1615, 3wcel 2105 . . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
1716, 13, 3wral 3138 . . . . . 6 wff 𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢
1810, 12, 17w3a 1079 . . . . 5 wff ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
1918, 7, 3wral 3138 . . . 4 wff 𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
204, 6, 19w3a 1079 . . 3 wff (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))
2120, 2cab 2799 . 2 class {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
221, 21wceq 1528 1 wff WUni = {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
Colors of variables: wff setvar class
This definition is referenced by:  iswun  10115
  Copyright terms: Public domain W3C validator