MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wun Structured version   Unicode version

Definition df-wun 8972
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 9010 of grothtsk 9105 in ZFC. (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
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 ) ) }
Distinct variable group:    x, y, u

Detailed syntax breakdown of Definition df-wun
StepHypRef Expression
1 cwun 8970 . 2  class WUni
2 vu . . . . . 6  setvar  u
32cv 1369 . . . . 5  class  u
43wtr 4485 . . . 4  wff  Tr  u
5 c0 3737 . . . . 5  class  (/)
63, 5wne 2644 . . . 4  wff  u  =/=  (/)
7 vx . . . . . . . . 9  setvar  x
87cv 1369 . . . . . . . 8  class  x
98cuni 4191 . . . . . . 7  class  U. x
109, 3wcel 1758 . . . . . 6  wff  U. x  e.  u
118cpw 3960 . . . . . . 7  class  ~P x
1211, 3wcel 1758 . . . . . 6  wff  ~P x  e.  u
13 vy . . . . . . . . . 10  setvar  y
1413cv 1369 . . . . . . . . 9  class  y
158, 14cpr 3979 . . . . . . . 8  class  { x ,  y }
1615, 3wcel 1758 . . . . . . 7  wff  { x ,  y }  e.  u
1716, 13, 3wral 2795 . . . . . 6  wff  A. y  e.  u  { x ,  y }  e.  u
1810, 12, 17w3a 965 . . . . 5  wff  ( U. x  e.  u  /\  ~P x  e.  u  /\  A. y  e.  u  { x ,  y }  e.  u )
1918, 7, 3wral 2795 . . . 4  wff  A. x  e.  u  ( U. x  e.  u  /\  ~P x  e.  u  /\  A. y  e.  u  { x ,  y }  e.  u )
204, 6, 19w3a 965 . . 3  wff  ( Tr  u  /\  u  =/=  (/)  /\  A. x  e.  u  ( U. x  e.  u  /\  ~P x  e.  u  /\  A. y  e.  u  { x ,  y }  e.  u ) )
2120, 2cab 2436 . 2  class  { u  |  ( Tr  u  /\  u  =/=  (/)  /\  A. x  e.  u  ( U. x  e.  u  /\  ~P x  e.  u  /\  A. y  e.  u  { x ,  y }  e.  u ) ) }
221, 21wceq 1370 1  wff 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 ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  iswun  8974
  Copyright terms: Public domain W3C validator