r1omfi

Description: Hereditarily finite sets are finite sets. (Contributed by BTernaryTau, 30-Dec-2025)

		Ref	Expression
	Assertion	r1omfi	$⊢ ⋃ R_{1} [ω] \subseteq Fin$

Step	Hyp	Ref	Expression
1		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
2	1	simpli	$⊢ Fun R_{1}$
3		eluniima	$⊢ Fun R_{1} \to (x \in ⋃ R_{1} [ω] \leftrightarrow \exists y \in ω x \in R_{1} (y))$
4	2 3	ax-mp	$⊢ x \in ⋃ R_{1} [ω] \leftrightarrow \exists y \in ω x \in R_{1} (y)$
5		r1fin	$⊢ y \in ω \to R_{1} (y) \in Fin$
6		r1pwss	$⊢ x \in R_{1} (y) \to 𝒫 x \subseteq R_{1} (y)$
7		ssfi	$⊢ (R_{1} (y) \in Fin \land 𝒫 x \subseteq R_{1} (y)) \to 𝒫 x \in Fin$
8	5 6 7	syl2an	$⊢ (y \in ω \land x \in R_{1} (y)) \to 𝒫 x \in Fin$
9	8	rexlimiva	$⊢ \exists y \in ω x \in R_{1} (y) \to 𝒫 x \in Fin$
10		pwfir	$⊢ 𝒫 x \in Fin \to x \in Fin$
11	9 10	syl	$⊢ \exists y \in ω x \in R_{1} (y) \to x \in Fin$
12	4 11	sylbi	$⊢ x \in ⋃ R_{1} [ω] \to x \in Fin$
13	12	ssriv	$⊢ ⋃ R_{1} [ω] \subseteq Fin$

Metamath Proof Explorer