Theorem dfhf2

Description: Alternate definition of the class of hereditarily finite sets as the value of the cumulative hierarchy of sets function at _om . This characterization is simpler but requires the axiom of infinity to hold. (Contributed by BTernaryTau, 25-Jan-2026) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026)

	Ref	Expression
Assertion	dfhf2	Could not format assertion : No typesetting found for |- HF = ( R1 ` _om ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		r1fun	$$⊢\mathrm{Fun}{R}_1$$
2		funiunfv	$$⊢\mathrm{Fun}{R}_1\to \bigcup _{x\in \mathrm{\omega }}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{\omega }\right]$$
3	1 2	ax-mp	$$⊢\bigcup _{x\in \mathrm{\omega }}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{\omega }\right]$$
4		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
5		limom	$$⊢\mathrm{Lim}\mathrm{\omega }$$
6		r1lim	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge \mathrm{Lim}\mathrm{\omega }\right)\to R_1\left(\mathrm{\omega }\right)=\bigcup _{x\in \mathrm{\omega }}{R}_1\left(x\right)$$
7	4 5 6	mp2an	$$⊢R_1\left(\mathrm{\omega }\right)=\bigcup _{x\in \mathrm{\omega }}{R}_1\left(x\right)$$
8		df-hf	Could not format HF = U. ( R1 " _om ) : No typesetting found for |- HF = U. ( R1 " _om ) with typecode |-
9	3 7 8	3eqtr4ri	Could not format HF = ( R1 ` _om ) : No typesetting found for |- HF = ( R1 ` _om ) with typecode |-