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

Definition df-wina 10108
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 Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 𝑦𝑧)}
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-wina
StepHypRef Expression
1 cwina 10106 . 2 class Inaccw
2 vx . . . . . 6 setvar 𝑥
32cv 1536 . . . . 5 class 𝑥
4 c0 4293 . . . . 5 class
53, 4wne 3018 . . . 4 wff 𝑥 ≠ ∅
6 ccf 9368 . . . . . 6 class cf
73, 6cfv 6357 . . . . 5 class (cf‘𝑥)
87, 3wceq 1537 . . . 4 wff (cf‘𝑥) = 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1536 . . . . . . 7 class 𝑦
11 vz . . . . . . . 8 setvar 𝑧
1211cv 1536 . . . . . . 7 class 𝑧
13 csdm 8510 . . . . . . 7 class
1410, 12, 13wbr 5068 . . . . . 6 wff 𝑦𝑧
1514, 11, 3wrex 3141 . . . . 5 wff 𝑧𝑥 𝑦𝑧
1615, 9, 3wral 3140 . . . 4 wff 𝑦𝑥𝑧𝑥 𝑦𝑧
175, 8, 16w3a 1083 . . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 𝑦𝑧)
1817, 2cab 2801 . 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 𝑦𝑧)}
191, 18wceq 1537 1 wff Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 𝑦𝑧)}
Colors of variables: wff setvar class
This definition is referenced by:  elwina  10110
  Copyright terms: Public domain W3C validator