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	⊢ HF = ( 𝑅1 ‘ ω )

Proof

Step	Hyp	Ref	Expression
1		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
2	1	simpli	⊢ Fun 𝑅1
3		funiunfv	⊢ ( Fun 𝑅1 → ∪ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ ω ) )
4	2 3	ax-mp	⊢ ∪ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = ∪ ( 𝑅1 “ ω )
5		omex	⊢ ω ∈ V
6		limom	⊢ Lim ω
7		r1lim	⊢ ( ( ω ∈ V ∧ Lim ω ) → ( 𝑅1 ‘ ω ) = ∪ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) )
8	5 6 7	mp2an	⊢ ( 𝑅1 ‘ ω ) = ∪ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 )
9		df-hf	⊢ HF = ∪ ( 𝑅1 “ ω )
10	4 8 9	3eqtr4ri	⊢ HF = ( 𝑅1 ‘ ω )