# 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 ${⊢}\mathrm{Inacc}=\left\{{x}|\left({x}\ne \varnothing \wedge \mathrm{cf}\left({x}\right)={x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}𝒫{y}\prec {x}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cina ${class}\mathrm{Inacc}$
1 vx ${setvar}{x}$
2 1 cv ${setvar}{x}$
3 c0 ${class}\varnothing$
4 2 3 wne ${wff}{x}\ne \varnothing$
5 ccf ${class}\mathrm{cf}$
6 2 5 cfv ${class}\mathrm{cf}\left({x}\right)$
7 6 2 wceq ${wff}\mathrm{cf}\left({x}\right)={x}$
8 vy ${setvar}{y}$
9 8 cv ${setvar}{y}$
10 9 cpw ${class}𝒫{y}$
11 csdm ${class}\prec$
12 10 2 11 wbr ${wff}𝒫{y}\prec {x}$
13 12 8 2 wral ${wff}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}𝒫{y}\prec {x}$
14 4 7 13 w3a ${wff}\left({x}\ne \varnothing \wedge \mathrm{cf}\left({x}\right)={x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}𝒫{y}\prec {x}\right)$
15 14 1 cab ${class}\left\{{x}|\left({x}\ne \varnothing \wedge \mathrm{cf}\left({x}\right)={x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}𝒫{y}\prec {x}\right)\right\}$
16 0 15 wceq ${wff}\mathrm{Inacc}=\left\{{x}|\left({x}\ne \varnothing \wedge \mathrm{cf}\left({x}\right)={x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}𝒫{y}\prec {x}\right)\right\}$