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 10459
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 10497) whereas the analogue for Grothendieck universes requires ax-groth 10580 (see grothtsk 10592). (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 10457 . 2 class WUni
2 vu . . . . . 6 setvar 𝑢
32cv 1541 . . . . 5 class 𝑢
43wtr 5196 . . . 4 wff Tr 𝑢
5 c0 4262 . . . . 5 class
63, 5wne 2945 . . . 4 wff 𝑢 ≠ ∅
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1541 . . . . . . . 8 class 𝑥
98cuni 4845 . . . . . . 7 class 𝑥
109, 3wcel 2110 . . . . . 6 wff 𝑥𝑢
118cpw 4539 . . . . . . 7 class 𝒫 𝑥
1211, 3wcel 2110 . . . . . 6 wff 𝒫 𝑥𝑢
13 vy . . . . . . . . . 10 setvar 𝑦
1413cv 1541 . . . . . . . . 9 class 𝑦
158, 14cpr 4569 . . . . . . . 8 class {𝑥, 𝑦}
1615, 3wcel 2110 . . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
1716, 13, 3wral 3066 . . . . . 6 wff 𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢
1810, 12, 17w3a 1086 . . . . 5 wff ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
1918, 7, 3wral 3066 . . . 4 wff 𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
204, 6, 19w3a 1086 . . 3 wff (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))
2120, 2cab 2717 . 2 class {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
221, 21wceq 1542 1 wff WUni = {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
Colors of variables: wff setvar class
This definition is referenced by:  iswun  10461
  Copyright terms: Public domain W3C validator