Theorem fineqvr1ombregs

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

	Ref	Expression
Assertion	fineqvr1ombregs	⊢ ( Fin = V ↔ ∪ ( 𝑅1 “ ω ) = V )

Proof

Step	Hyp	Ref	Expression
1		fineqvomon	⊢ ( Fin = V → ω = On )
2	1	imaeq2d	⊢ ( Fin = V → ( 𝑅1 “ ω ) = ( 𝑅1 “ On ) )
3	2	unieqd	⊢ ( Fin = V → ∪ ( 𝑅1 “ ω ) = ∪ ( 𝑅1 “ On ) )
4		unir1regs	⊢ ∪ ( 𝑅1 “ On ) = V
5	3 4	eqtrdi	⊢ ( Fin = V → ∪ ( 𝑅1 “ ω ) = V )
6		r1omfi	⊢ ∪ ( 𝑅1 “ ω ) ⊆ Fin
7		sseq1	⊢ ( ∪ ( 𝑅1 “ ω ) = V → ( ∪ ( 𝑅1 “ ω ) ⊆ Fin ↔ V ⊆ Fin ) )
8	6 7	mpbii	⊢ ( ∪ ( 𝑅1 “ ω ) = V → V ⊆ Fin )
9		vss	⊢ ( V ⊆ Fin ↔ Fin = V )
10	8 9	sylib	⊢ ( ∪ ( 𝑅1 “ ω ) = V → Fin = V )
11	5 10	impbii	⊢ ( Fin = V ↔ ∪ ( 𝑅1 “ ω ) = V )