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

Definition df-ina 8550
Description: An ordinal is strongly inaccessible iff it is a regular strong limit cardinal, which is to say that it dominates the powersets of every smaller ordinal. (Contributed by Mario Carneiro, 22-Jun-2013.)
Assertion
Ref Expression
df-ina  |-  Inacc  =  {
x  |  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  ~P y  ~<  x ) }
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-ina
StepHypRef Expression
1 cina 8548 . 2  class  Inacc
2 vx . . . . . 6  set  x
32cv 1651 . . . . 5  class  x
4 c0 3620 . . . . 5  class  (/)
53, 4wne 2598 . . . 4  wff  x  =/=  (/)
6 ccf 7814 . . . . . 6  class  cf
73, 6cfv 5446 . . . . 5  class  ( cf `  x )
87, 3wceq 1652 . . . 4  wff  ( cf `  x )  =  x
9 vy . . . . . . . 8  set  y
109cv 1651 . . . . . . 7  class  y
1110cpw 3791 . . . . . 6  class  ~P y
12 csdm 7100 . . . . . 6  class  ~<
1311, 3, 12wbr 4204 . . . . 5  wff  ~P y  ~<  x
1413, 9, 3wral 2697 . . . 4  wff  A. y  e.  x  ~P y  ~<  x
155, 8, 14w3a 936 . . 3  wff  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  ~P y  ~<  x )
1615, 2cab 2421 . 2  class  { x  |  ( x  =/=  (/)  /\  ( cf `  x
)  =  x  /\  A. y  e.  x  ~P y  ~<  x ) }
171, 16wceq 1652 1  wff  Inacc  =  {
x  |  ( x  =/=  (/)  /\  ( cf `  x )  =  x  /\  A. y  e.  x  ~P y  ~<  x ) }
Colors of variables: wff set class
This definition is referenced by:  elina  8552
  Copyright terms: Public domain W3C validator