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 9491
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 9489 . 2 class Inaccw
2 vx . . . . . 6 setvar 𝑥
32cv 1480 . . . . 5 class 𝑥
4 c0 3907 . . . . 5 class
53, 4wne 2791 . . . 4 wff 𝑥 ≠ ∅
6 ccf 8748 . . . . . 6 class cf
73, 6cfv 5876 . . . . 5 class (cf‘𝑥)
87, 3wceq 1481 . . . 4 wff (cf‘𝑥) = 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1480 . . . . . . 7 class 𝑦
11 vz . . . . . . . 8 setvar 𝑧
1211cv 1480 . . . . . . 7 class 𝑧
13 csdm 7939 . . . . . . 7 class
1410, 12, 13wbr 4644 . . . . . 6 wff 𝑦𝑧
1514, 11, 3wrex 2910 . . . . 5 wff 𝑧𝑥 𝑦𝑧
1615, 9, 3wral 2909 . . . 4 wff 𝑦𝑥𝑧𝑥 𝑦𝑧
175, 8, 16w3a 1036 . . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 𝑦𝑧)
1817, 2cab 2606 . 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 𝑦𝑧)}
191, 18wceq 1481 1 wff Inaccw = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥𝑧𝑥 𝑦𝑧)}
Colors of variables: wff setvar class
This definition is referenced by:  elwina  9493
  Copyright terms: Public domain W3C validator