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	Could not format assertion : No typesetting found for |- ( Fin = _V <-> HF = _V ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-hf	Could not format HF = U. ( R1 " _om ) : No typesetting found for |- HF = U. ( R1 " _om ) with typecode |-
2		fineqvomon	$$⊢\mathrm{Fin}=\mathrm{V}\to \mathrm{\omega }=\mathrm{On}$$
3	2	imaeq2d	$$⊢\mathrm{Fin}=\mathrm{V}\to R_1\left[\mathrm{\omega }\right]=R_1\left[\mathrm{On}\right]$$
4	3	unieqd	$$⊢\mathrm{Fin}=\mathrm{V}\to \bigcup R_1\left[\mathrm{\omega }\right]=\bigcup R_1\left[\mathrm{On}\right]$$
5	1 4	eqtrid	Could not format ( Fin = _V -> HF = U. ( R1 " On ) ) : No typesetting found for |- ( Fin = _V -> HF = U. ( R1 " On ) ) with typecode |-
6		unir1regs	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$
7	5 6	eqtrdi	Could not format ( Fin = _V -> HF = _V ) : No typesetting found for |- ( Fin = _V -> HF = _V ) with typecode |-
8		hffi	Could not format ( x e. HF -> x e. Fin ) : No typesetting found for |- ( x e. HF -> x e. Fin ) with typecode |-
9	8	ssriv	Could not format HF C_ Fin : No typesetting found for |- HF C_ Fin with typecode |-
10		sseq1	Could not format ( HF = _V -> ( HF C_ Fin <-> _V C_ Fin ) ) : No typesetting found for |- ( HF = _V -> ( HF C_ Fin <-> _V C_ Fin ) ) with typecode |-
11	9 10	mpbii	Could not format ( HF = _V -> _V C_ Fin ) : No typesetting found for |- ( HF = _V -> _V C_ Fin ) with typecode |-
12		vss	$$⊢\mathrm{V}\subseteq \mathrm{Fin}\leftrightarrow \mathrm{Fin}=\mathrm{V}$$
13	11 12	sylib	Could not format ( HF = _V -> Fin = _V ) : No typesetting found for |- ( HF = _V -> Fin = _V ) with typecode |-
14	7 13	impbii	Could not format ( Fin = _V <-> HF = _V ) : No typesetting found for |- ( Fin = _V <-> HF = _V ) with typecode |-