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

Definition df-wina 8856
Description: An ordinal is weakly inaccessible iff it is a regular limit cardinal. Note that our definition allows  om as a weakly inaccessible cardinal. (Contributed by Mario Carneiro, 22-Jun-2013.)
Assertion
Ref Expression
df-wina  |-  InaccW  =  { x  |  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  E. z  e.  x  y  ~<  z ) }
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-wina
StepHypRef Expression
1 cwina 8854 . 2  class  InaccW
2 vx . . . . . 6  setvar  x
32cv 1368 . . . . 5  class  x
4 c0 3642 . . . . 5  class  (/)
53, 4wne 2611 . . . 4  wff  x  =/=  (/)
6 ccf 8112 . . . . . 6  class  cf
73, 6cfv 5423 . . . . 5  class  ( cf `  x )
87, 3wceq 1369 . . . 4  wff  ( cf `  x )  =  x
9 vy . . . . . . . 8  setvar  y
109cv 1368 . . . . . . 7  class  y
11 vz . . . . . . . 8  setvar  z
1211cv 1368 . . . . . . 7  class  z
13 csdm 7314 . . . . . . 7  class  ~<
1410, 12, 13wbr 4297 . . . . . 6  wff  y  ~< 
z
1514, 11, 3wrex 2721 . . . . 5  wff  E. z  e.  x  y  ~<  z
1615, 9, 3wral 2720 . . . 4  wff  A. y  e.  x  E. z  e.  x  y  ~<  z
175, 8, 16w3a 965 . . 3  wff  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  E. z  e.  x  y  ~<  z
)
1817, 2cab 2429 . 2  class  { x  |  ( x  =/=  (/)  /\  ( cf `  x
)  =  x  /\  A. y  e.  x  E. z  e.  x  y  ~<  z ) }
191, 18wceq 1369 1  wff  InaccW  =  { x  |  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  E. z  e.  x  y  ~<  z ) }
Colors of variables: wff setvar class
This definition is referenced by:  elwina  8858
  Copyright terms: Public domain W3C validator