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

Definition df-wun 9083
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 9121 of grothtsk 9216 in ZFC (whereas grothtsk 9216 requires ax-groth 9204). (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 9081 . 2  class WUni
2 vu . . . . . 6  setvar  u
32cv 1382 . . . . 5  class  u
43wtr 4530 . . . 4  wff  Tr  u
5 c0 3770 . . . . 5  class  (/)
63, 5wne 2638 . . . 4  wff  u  =/=  (/)
7 vx . . . . . . . . 9  setvar  x
87cv 1382 . . . . . . . 8  class  x
98cuni 4234 . . . . . . 7  class  U. x
109, 3wcel 1804 . . . . . 6  wff  U. x  e.  u
118cpw 3997 . . . . . . 7  class  ~P x
1211, 3wcel 1804 . . . . . 6  wff  ~P x  e.  u
13 vy . . . . . . . . . 10  setvar  y
1413cv 1382 . . . . . . . . 9  class  y
158, 14cpr 4016 . . . . . . . 8  class  { x ,  y }
1615, 3wcel 1804 . . . . . . 7  wff  { x ,  y }  e.  u
1716, 13, 3wral 2793 . . . . . 6  wff  A. y  e.  u  { x ,  y }  e.  u
1810, 12, 17w3a 974 . . . . 5  wff  ( U. x  e.  u  /\  ~P x  e.  u  /\  A. y  e.  u  { x ,  y }  e.  u )
1918, 7, 3wral 2793 . . . 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 974 . . 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 2428 . 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 1383 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  9085
  Copyright terms: Public domain W3C validator