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 9795
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 9793 . 2 class Inacc
2 vx . . . . . 6 setvar 𝑥
32cv 1652 . . . . 5 class 𝑥
4 c0 4115 . . . . 5 class
53, 4wne 2971 . . . 4 wff 𝑥 ≠ ∅
6 ccf 9049 . . . . . 6 class cf
73, 6cfv 6101 . . . . 5 class (cf‘𝑥)
87, 3wceq 1653 . . . 4 wff (cf‘𝑥) = 𝑥
9 vy . . . . . . . 8 setvar 𝑦
109cv 1652 . . . . . . 7 class 𝑦
1110cpw 4349 . . . . . 6 class 𝒫 𝑦
12 csdm 8194 . . . . . 6 class
1311, 3, 12wbr 4843 . . . . 5 wff 𝒫 𝑦𝑥
1413, 9, 3wral 3089 . . . 4 wff 𝑦𝑥 𝒫 𝑦𝑥
155, 8, 14w3a 1108 . . 3 wff (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥 𝒫 𝑦𝑥)
1615, 2cab 2785 . 2 class {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥 𝒫 𝑦𝑥)}
171, 16wceq 1653 1 wff Inacc = {𝑥 ∣ (𝑥 ≠ ∅ ∧ (cf‘𝑥) = 𝑥 ∧ ∀𝑦𝑥 𝒫 𝑦𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  elina  9797
  Copyright terms: Public domain W3C validator