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 definition is simpler but requires Infinity to work. (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		r1funlim	$$⊢\left(\mathrm{Fun}{R}_1\wedge \mathrm{Lim}\mathrm{dom}{R}_1\right)$$
2	1	simpli	$$⊢\mathrm{Fun}{R}_1$$
3		funiunfv	$$⊢\mathrm{Fun}{R}_1\to \bigcup _{x\in \mathrm{\omega }}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{\omega }\right]$$
4	2 3	ax-mp	$$⊢\bigcup _{x\in \mathrm{\omega }}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{\omega }\right]$$
5		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
6		limom	$$⊢\mathrm{Lim}\mathrm{\omega }$$
7		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)$$
8	5 6 7	mp2an	$$⊢R_1\left(\mathrm{\omega }\right)=\bigcup _{x\in \mathrm{\omega }}{R}_1\left(x\right)$$
9		df-hf	Could not format HF = U. ( R1 " _om ) : No typesetting found for |- HF = U. ( R1 " _om ) with typecode |-
10	4 8 9	3eqtr4ri	Could not format HF = ( R1 ` _om ) : No typesetting found for |- HF = ( R1 ` _om ) with typecode |-