Theorem r1omfi

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

	Ref	Expression
Assertion	r1omfi	⊢ ∪ ( 𝑅1 “ ω ) ⊆ Fin

Proof

Step	Hyp	Ref	Expression
1		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
2	1	simpli	⊢ Fun 𝑅1
3		eluniima	⊢ ( Fun 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
4	2 3	ax-mp	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
5		r1fin	⊢ ( 𝑦 ∈ ω → ( 𝑅1 ‘ 𝑦 ) ∈ Fin )
6		r1pwss	⊢ ( 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝒫 𝑥 ⊆ ( 𝑅1 ‘ 𝑦 ) )
7		ssfi	⊢ ( ( ( 𝑅1 ‘ 𝑦 ) ∈ Fin ∧ 𝒫 𝑥 ⊆ ( 𝑅1 ‘ 𝑦 ) ) → 𝒫 𝑥 ∈ Fin )
8	5 6 7	syl2an	⊢ ( ( 𝑦 ∈ ω ∧ 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) → 𝒫 𝑥 ∈ Fin )
9	8	rexlimiva	⊢ ( ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝒫 𝑥 ∈ Fin )
10		pwfir	⊢ ( 𝒫 𝑥 ∈ Fin → 𝑥 ∈ Fin )
11	9 10	syl	⊢ ( ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝑥 ∈ Fin )
12	4 11	sylbi	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ ω ) → 𝑥 ∈ Fin )
13	12	ssriv	⊢ ∪ ( 𝑅1 “ ω ) ⊆ Fin