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

Definition df-wina 9083
Description: An ordinal is weakly inaccessible iff it is a regular limit cardinal. Note that our definition allows as a weakly inaccessible cardinal. (Contributed by Mario Carneiro, 22-Jun-2013.)
Assertion
Ref Expression
df-wina
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-wina
StepHypRef Expression
1 cwina 9081 . 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
11 vz . . . . . . . 8
1211cv 1394 . . . . . . 7
13 csdm 7535 . . . . . . 7
1410, 12, 13wbr 4452 . . . . . 6
1514, 11, 3wrex 2808 . . . . 5
1615, 9, 3wral 2807 . . . 4
175, 8, 16w3a 973 . . 3
1817, 2cab 2442 . 2
191, 18wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  elwina  9085
  Copyright terms: Public domain W3C validator