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\exists z\in xy\prec z\right)\right\}$$

Detailed syntax breakdown

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