This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ina

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)

Ref Expression
Assertion df-ina ⊢ Inacc = x | x ≠ ∅ ∧ cf ⁡ x = x ∧ ∀ y ∈ x 𝒫 y ≺ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cina class Inacc
1 vx setvar x
2 1 cv setvar x
3 c0 class ∅
4 2 3 wne wff x ≠ ∅
5 ccf class cf
6 2 5 cfv class cf ⁡ x
7 6 2 wceq wff cf ⁡ x = x
8 vy setvar y
9 8 cv setvar y
10 9 cpw class 𝒫 y
11 csdm class ≺
12 10 2 11 wbr wff 𝒫 y ≺ x
13 12 8 2 wral wff ∀ y ∈ x 𝒫 y ≺ x
14 4 7 13 w3a wff x ≠ ∅ ∧ cf ⁡ x = x ∧ ∀ y ∈ x 𝒫 y ≺ x
15 14 1 cab class x | x ≠ ∅ ∧ cf ⁡ x = x ∧ ∀ y ∈ x 𝒫 y ≺ x
16 0 15 wceq wff Inacc = x | x ≠ ∅ ∧ cf ⁡ x = x ∧ ∀ y ∈ x 𝒫 y ≺ x