Metamath Proof Explorer

Definition df-wun

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 ) whereas the analogue for Grothendieck universes requires ax-groth (see grothtsk ). (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-wun ⊢ WUni = u | Tr ⁡ u ∧ u ≠ ∅ ∧ ∀ x ∈ u ⋃ x ∈ u ∧ 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwun class WUni
1 vu setvar u
2 1 cv setvar u
3 2 wtr wff Tr ⁡ u
4 c0 class ∅
5 2 4 wne wff u ≠ ∅
6 vx setvar x
7 6 cv setvar x
8 7 cuni class ⋃ x
9 8 2 wcel wff ⋃ x ∈ u
10 7 cpw class 𝒫 x
11 10 2 wcel wff 𝒫 x ∈ u
12 vy setvar y
13 12 cv setvar y
14 7 13 cpr class x y
15 14 2 wcel wff x y ∈ u
16 15 12 2 wral wff ∀ y ∈ u x y ∈ u
17 9 11 16 w3a wff ⋃ x ∈ u ∧ 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u
18 17 6 2 wral wff ∀ x ∈ u ⋃ x ∈ u ∧ 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u
19 3 5 18 w3a wff Tr ⁡ u ∧ u ≠ ∅ ∧ ∀ x ∈ u ⋃ x ∈ u ∧ 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u
20 19 1 cab class u | Tr ⁡ u ∧ u ≠ ∅ ∧ ∀ x ∈ u ⋃ x ∈ u ∧ 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u
21 0 20 wceq wff WUni = u | Tr ⁡ u ∧ u ≠ ∅ ∧ ∀ x ∈ u ⋃ x ∈ u ∧ 𝒫 x ∈ u ∧ ∀ y ∈ u x y ∈ u