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 = U. ( R1 " _om )
2		fineqvomon	|- ( Fin = _V -> _om = On )
3	2	imaeq2d	|- ( Fin = _V -> ( R1 " _om ) = ( R1 " On ) )
4	3	unieqd	|- ( Fin = _V -> U. ( R1 " _om ) = U. ( R1 " On ) )
5	1 4	eqtrid	|- ( Fin = _V -> HF = U. ( R1 " On ) )
6		unir1regs	|- U. ( R1 " On ) = _V
7	5 6	eqtrdi	|- ( Fin = _V -> HF = _V )
8		hffi	|- ( x e. HF -> x e. Fin )
9	8	ssriv	|- HF C_ Fin
10		sseq1	|- ( HF = _V -> ( HF C_ Fin <-> _V C_ Fin ) )
11	9 10	mpbii	|- ( HF = _V -> _V C_ Fin )
12		vss	|- ( _V C_ Fin <-> Fin = _V )
13	11 12	sylib	|- ( HF = _V -> Fin = _V )
14	7 13	impbii	|- ( Fin = _V <-> HF = _V )