Definition df-hf

Description: Define the class of sets belonging to the finite stages of the cumulative hierarchy of sets. This is the class of sets of finite rank by elhf2 . They are called the hereditarily finite sets since they are the finite sets whose members are hereditarily finite, as proved in elhf3 . (Contributed by Scott Fenton, 9-Jul-2015)

	Ref	Expression
Assertion	df-hf	Could not format assertion : No typesetting found for |- HF = U. ( R1 " _om ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chf	Could not format HF : No typesetting found for class HF with typecode class
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	Could not format HF = U. ( R1 " _om ) : No typesetting found for wff HF = U. ( R1 " _om ) with typecode wff