Theorem fineqvhfbregs

Description: All sets are finite iff all sets are hereditarily finite. (Contributed by BTernaryTau, 30-Dec-2025) Use HF . (Revised by BTernaryTau, 24-Oct-2026)

	Ref	Expression
Assertion	fineqvhfbregs	⊢ ( Fin = V ↔ HF = V )

Proof

Step	Hyp	Ref	Expression
1		df-hf	⊢ HF = ∪ ( 𝑅1 “ ω )
2		fineqvomon	⊢ ( Fin = V → ω = On )
3	2	imaeq2d	⊢ ( Fin = V → ( 𝑅1 “ ω ) = ( 𝑅1 “ On ) )
4	3	unieqd	⊢ ( Fin = V → ∪ ( 𝑅1 “ ω ) = ∪ ( 𝑅1 “ On ) )
5	1 4	eqtrid	⊢ ( Fin = V → HF = ∪ ( 𝑅1 “ On ) )
6		unir1regs	⊢ ∪ ( 𝑅1 “ On ) = V
7	5 6	eqtrdi	⊢ ( Fin = V → HF = V )
8		hffi	⊢ ( 𝑥 ∈ HF → 𝑥 ∈ Fin )
9	8	ssriv	⊢ HF ⊆ Fin
10		sseq1	⊢ ( HF = V → ( HF ⊆ Fin ↔ V ⊆ Fin ) )
11	9 10	mpbii	⊢ ( HF = V → V ⊆ Fin )
12		vss	⊢ ( V ⊆ Fin ↔ Fin = V )
13	11 12	sylib	⊢ ( HF = V → Fin = V )
14	7 13	impbii	⊢ ( Fin = V ↔ HF = V )