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 10329
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 10327 . 2 class Inacc
2 vx . . . . . 6 setvar 𝑥
32cv 1542 . . . . 5 class 𝑥
4 c0 4254 . . . . 5 class
53, 4wne 2943 . . . 4 wff 𝑥 ≠ ∅
6 ccf 9583 . . . . . 6 class cf
73, 6cfv 6401 . . . . 5 class (cf‘𝑥)
87, 3wceq 1543 . . . 4 wff (cf‘𝑥) = 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1542 . . . . . . 7 class 𝑦
1110cpw 4530 . . . . . 6 class 𝒫 𝑦
12 csdm 8649 . . . . . 6 class
1311, 3, 12wbr 5070 . . . . 5 wff 𝒫 𝑦𝑥
1413, 9, 3wral 3064 . . . 4 wff 𝑦𝑥 𝒫 𝑦𝑥
155, 8, 14w3a 1089 . . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥 𝒫 𝑦𝑥)
1615, 2cab 2716 . 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥 𝒫 𝑦𝑥)}
171, 16wceq 1543 1 wff Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥 𝒫 𝑦𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  elina  10331
  Copyright terms: Public domain W3C validator