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 9468
Description: The class of all weak universes. A weak universe is a nonempty transitive class closed under union, pairing, and powerset. The advantage of a weak universe over a Grothendieck universe is that weak universes satisfy the analogue uniwun 9506 of grothtsk 9601 in ZFC (whereas grothtsk 9601 requires ax-groth 9589). (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 9466 . 2 class WUni
2 vu . . . . . 6 setvar 𝑢
32cv 1479 . . . . 5 class 𝑢
43wtr 4712 . . . 4 wff Tr 𝑢
5 c0 3891 . . . . 5 class
63, 5wne 2790 . . . 4 wff 𝑢 ≠ ∅
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1479 . . . . . . . 8 class 𝑥
98cuni 4402 . . . . . . 7 class 𝑥
109, 3wcel 1987 . . . . . 6 wff 𝑥𝑢
118cpw 4130 . . . . . . 7 class 𝒫 𝑥
1211, 3wcel 1987 . . . . . 6 wff 𝒫 𝑥𝑢
13 vy . . . . . . . . . 10 setvar 𝑦
1413cv 1479 . . . . . . . . 9 class 𝑦
158, 14cpr 4150 . . . . . . . 8 class {𝑥, 𝑦}
1615, 3wcel 1987 . . . . . . 7 wff {𝑥, 𝑦} ∈ 𝑢
1716, 13, 3wral 2907 . . . . . 6 wff 𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢
1810, 12, 17w3a 1036 . . . . 5 wff ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
1918, 7, 3wral 2907 . . . 4 wff 𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢)
204, 6, 19w3a 1036 . . 3 wff (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))
2120, 2cab 2607 . 2 class {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
221, 21wceq 1480 1 wff WUni = {𝑢 ∣ (Tr 𝑢𝑢 ≠ ∅ ∧ ∀𝑥𝑢 ( 𝑥𝑢 ∧ 𝒫 𝑥𝑢 ∧ ∀𝑦𝑢 {𝑥, 𝑦} ∈ 𝑢))}
Colors of variables: wff setvar class
This definition is referenced by:  iswun  9470
  Copyright terms: Public domain W3C validator