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

Definition df-ina 9084
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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-ina
StepHypRef Expression
1 cina 9082 . 2
2 vx . . . . . 6
32cv 1394 . . . . 5
4 c0 3784 . . . . 5
53, 4wne 2652 . . . 4
6 ccf 8339 . . . . . 6
73, 6cfv 5593 . . . . 5
87, 3wceq 1395 . . . 4
9 vy . . . . . . . 8
109cv 1394 . . . . . . 7
1110cpw 4012 . . . . . 6
12 csdm 7535 . . . . . 6
1311, 3, 12wbr 4452 . . . . 5
1413, 9, 3wral 2807 . . . 4
155, 8, 14w3a 973 . . 3
1615, 2cab 2442 . 2
171, 16wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  elina  9086
  Copyright terms: Public domain W3C validator