Definition df-hf

Description: Define the hereditarily finite sets. These are the finite sets whose elements are finite, and so forth. (Contributed by Scott Fenton, 9-Jul-2015)

	Ref	Expression
Assertion	df-hf	$$⊢\mathrm{Hf}=\bigcup R_1\left[\mathrm{\omega }\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chf	$$class\mathrm{Hf}$$
1		cr1	$$class{R}_1$$
2		com	$$class\mathrm{\omega }$$
3	1 2	cima	$$class{R}_1\left[\mathrm{\omega }\right]$$
4	3	cuni	$$class\bigcup R_1\left[\mathrm{\omega }\right]$$
5	0 4	wceq	$$wff\mathrm{Hf}=\bigcup R_1\left[\mathrm{\omega }\right]$$