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

Definition df-wun 8340
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 8378 of grothtsk 8473 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 8338 . 2  class WUni
2 vu . . . . . 6  set  u
32cv 1631 . . . . 5  class  u
43wtr 4129 . . . 4  wff  Tr  u
5 c0 3468 . . . . 5  class  (/)
63, 5wne 2459 . . . 4  wff  u  =/=  (/)
7 vx . . . . . . . . 9  set  x
87cv 1631 . . . . . . . 8  class  x
98cuni 3843 . . . . . . 7  class  U. x
109, 3wcel 1696 . . . . . 6  wff  U. x  e.  u
118cpw 3638 . . . . . . 7  class  ~P x
1211, 3wcel 1696 . . . . . 6  wff  ~P x  e.  u
13 vy . . . . . . . . . 10  set  y
1413cv 1631 . . . . . . . . 9  class  y
158, 14cpr 3654 . . . . . . . 8  class  { x ,  y }
1615, 3wcel 1696 . . . . . . 7  wff  { x ,  y }  e.  u
1716, 13, 3wral 2556 . . . . . 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 2556 . . . 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 2282 . 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 1632 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  8342
  Copyright terms: Public domain W3C validator