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𝒫y\prec x\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cina	$$class\mathrm{Inacc}$$
1		vx	$$setvarx$$
2	1	cv	$$setvarx$$
3		c0	$$class\varnothing$$
4	2 3	wne	$$wffx\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	$$setvary$$
9	8	cv	$$setvary$$
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𝒫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𝒫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𝒫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𝒫y\prec x\right)\right\}$$