This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) }