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

Proof

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