Theorem fineqvr1ombregs

Description: All sets are finite iff all sets are hereditarily finite. (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	fineqvr1ombregs	$$⊢\mathrm{Fin}=\mathrm{V}\leftrightarrow \bigcup R_1\left[\mathrm{\omega }\right]=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fineqvomon	$$⊢\mathrm{Fin}=\mathrm{V}\to \mathrm{\omega }=\mathrm{On}$$
2	1	imaeq2d	$$⊢\mathrm{Fin}=\mathrm{V}\to R_1\left[\mathrm{\omega }\right]=R_1\left[\mathrm{On}\right]$$
3	2	unieqd	$$⊢\mathrm{Fin}=\mathrm{V}\to \bigcup R_1\left[\mathrm{\omega }\right]=\bigcup R_1\left[\mathrm{On}\right]$$
4		unir1regs	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$
5	3 4	eqtrdi	$$⊢\mathrm{Fin}=\mathrm{V}\to \bigcup R_1\left[\mathrm{\omega }\right]=\mathrm{V}$$
6		r1omfi	$$⊢\bigcup R_1\left[\mathrm{\omega }\right]\subseteq \mathrm{Fin}$$
7		sseq1	$$⊢\bigcup R_1\left[\mathrm{\omega }\right]=\mathrm{V}\to \left(\bigcup R_1\left[\mathrm{\omega }\right]\subseteq \mathrm{Fin}\leftrightarrow \mathrm{V}\subseteq \mathrm{Fin}\right)$$
8	6 7	mpbii	$$⊢\bigcup R_1\left[\mathrm{\omega }\right]=\mathrm{V}\to \mathrm{V}\subseteq \mathrm{Fin}$$
9		vss	$$⊢\mathrm{V}\subseteq \mathrm{Fin}\leftrightarrow \mathrm{Fin}=\mathrm{V}$$
10	8 9	sylib	$$⊢\bigcup R_1\left[\mathrm{\omega }\right]=\mathrm{V}\to \mathrm{Fin}=\mathrm{V}$$
11	5 10	impbii	$$⊢\mathrm{Fin}=\mathrm{V}\leftrightarrow \bigcup R_1\left[\mathrm{\omega }\right]=\mathrm{V}$$