Theorem r1omfi

Description: Obsolete theorem, use hffi instead. Hereditarily finite sets are finite sets. (Contributed by BTernaryTau, 30-Dec-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	r1omfi	$$⊢\bigcup R_1\left[\mathrm{\omega }\right]\subseteq \mathrm{Fin}$$

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	1	eleq2i	Could not format ( x e. HF <-> x e. U. ( R1 " _om ) ) : No typesetting found for |- ( x e. HF <-> x e. U. ( R1 " _om ) ) with typecode |-
3		hffi	Could not format ( x e. HF -> x e. Fin ) : No typesetting found for |- ( x e. HF -> x e. Fin ) with typecode |-
4	2 3	sylbir	$$⊢x\in \bigcup R_1\left[\mathrm{\omega }\right]\to x\in \mathrm{Fin}$$
5	4	ssriv	$$⊢\bigcup R_1\left[\mathrm{\omega }\right]\subseteq \mathrm{Fin}$$