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 =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwun
 |-  WUni
1 vu
 |-  u
2 1 cv
 |-  u
3 2 wtr
 |-  Tr u
4 c0
 |-  (/)
5 2 4 wne
 |-  u =/= (/)
6 vx
 |-  x
7 6 cv
 |-  x
8 7 cuni
 |-  U. x
9 8 2 wcel
 |-  U. x e. u
10 7 cpw
 |-  ~P x
11 10 2 wcel
 |-  ~P x e. u
12 vy
 |-  y
13 12 cv
 |-  y
14 7 13 cpr
 |-  { x , y }
15 14 2 wcel
 |-  { x , y } e. u
16 15 12 2 wral
 |-  A. y e. u { x , y } e. u
17 9 11 16 w3a
 |-  ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u )
18 17 6 2 wral
 |-  A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u )
19 3 5 18 w3a
 |-  ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) )
20 19 1 cab
 |-  { u | ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) }
21 0 20 wceq
 |-  WUni = { u | ( Tr u /\ u =/= (/) /\ A. x e. u ( U. x e. u /\ ~P x e. u /\ A. y e. u { x , y } e. u ) ) }