# Metamath Proof Explorer

## Definition df-wina

Description: An ordinal is weakly inaccessible iff it is a regular limit cardinal. Note that our definition allows _om as a weakly inaccessible cardinal. (Contributed by Mario Carneiro, 22-Jun-2013)

Ref Expression
Assertion df-wina ${⊢}{\mathrm{Inacc}}_{𝑤}=\left\{{x}|\left({x}\ne \varnothing \wedge \mathrm{cf}\left({x}\right)={x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}\prec {z}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cwina ${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 vz ${setvar}{z}$
10 8 cv ${setvar}{y}$
11 csdm ${class}\prec$
12 9 cv ${setvar}{z}$
13 10 12 11 wbr ${wff}{y}\prec {z}$
14 13 9 2 wrex ${wff}\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}\prec {z}$
15 14 8 2 wral ${wff}\forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}\prec {z}$
16 4 7 15 w3a ${wff}\left({x}\ne \varnothing \wedge \mathrm{cf}\left({x}\right)={x}\wedge \forall {y}\in {x}\phantom{\rule{.4em}{0ex}}\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}\prec {z}\right)$
17 16 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}}\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}\prec {z}\right)\right\}$
18 0 17 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}}\exists {z}\in {x}\phantom{\rule{.4em}{0ex}}{y}\prec {z}\right)\right\}$