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

Definition df-wun 8324
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 8362 of grothtsk 8457 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 8322 . 2  class WUni
2 vu . . . . . 6  set  u
32cv 1622 . . . . 5  class  u
43wtr 4113 . . . 4  wff  Tr  u
5 c0 3455 . . . . 5  class  (/)
63, 5wne 2446 . . . 4  wff  u  =/=  (/)
7 vx . . . . . . . . 9  set  x
87cv 1622 . . . . . . . 8  class  x
98cuni 3827 . . . . . . 7  class  U. x
109, 3wcel 1684 . . . . . 6  wff  U. x  e.  u
118cpw 3625 . . . . . . 7  class  ~P x
1211, 3wcel 1684 . . . . . 6  wff  ~P x  e.  u
13 vy . . . . . . . . . 10  set  y
1413cv 1622 . . . . . . . . 9  class  y
158, 14cpr 3641 . . . . . . . 8  class  { x ,  y }
1615, 3wcel 1684 . . . . . . 7  wff  { x ,  y }  e.  u
1716, 13, 3wral 2543 . . . . . 6  wff  A. y  e.  u  { x ,  y }  e.  u
1810, 12, 17w3a 934 . . . . 5  wff  ( U. x  e.  u  /\  ~P x  e.  u  /\  A. y  e.  u  { x ,  y }  e.  u )
1918, 7, 3wral 2543 . . . 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 934 . . 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 2269 . 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 1623 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 set class
This definition is referenced by:  iswun  8326
  Copyright terms: Public domain W3C validator