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

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

Detailed syntax breakdown of Definition df-ina
StepHypRef Expression
1 cina 9502 . 2 class Inacc
2 vx . . . . . 6 setvar 𝑥
32cv 1481 . . . . 5 class 𝑥
4 c0 3913 . . . . 5 class
53, 4wne 2793 . . . 4 wff 𝑥 ≠ ∅
6 ccf 8760 . . . . . 6 class cf
73, 6cfv 5886 . . . . 5 class (cf‘𝑥)
87, 3wceq 1482 . . . 4 wff (cf‘𝑥) = 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1481 . . . . . . 7 class 𝑦
1110cpw 4156 . . . . . 6 class 𝒫 𝑦
12 csdm 7951 . . . . . 6 class
1311, 3, 12wbr 4651 . . . . 5 wff 𝒫 𝑦𝑥
1413, 9, 3wral 2911 . . . 4 wff 𝑦𝑥 𝒫 𝑦𝑥
155, 8, 14w3a 1037 . . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥 𝒫 𝑦𝑥)
1615, 2cab 2607 . 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥 𝒫 𝑦𝑥)}
171, 16wceq 1482 1 wff Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥 𝒫 𝑦𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  elina  9506
  Copyright terms: Public domain W3C validator