Theorem r1omhf

Description: A set is hereditarily finite iff it is finite and all of its elements are hereditarily finite. (Contributed by BTernaryTau, 19-Jan-2026)

	Ref	Expression
Assertion	r1omhf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) ↔ ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) )

Proof

Step	Hyp	Ref	Expression
1		r1omfi	⊢ ∪ ( 𝑅1 “ ω ) ⊆ Fin
2	1	sseli	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) → 𝐴 ∈ Fin )
3		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
4	3	simpli	⊢ Fun 𝑅1
5		eluniima	⊢ ( Fun 𝑅1 → ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑦 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
6	4 5	ax-mp	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑦 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) )
7		r19.41v	⊢ ( ∃ 𝑦 ∈ ω ( 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) ↔ ( ∃ 𝑦 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) )
8		r1elcl	⊢ ( ( 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
9	8	reximi	⊢ ( ∃ 𝑦 ∈ ω ( 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
10	7 9	sylbir	⊢ ( ( ∃ 𝑦 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
11	6 10	sylanb	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
12		eluniima	⊢ ( Fun 𝑅1 → ( 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
13	4 12	ax-mp	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
14	11 13	sylibr	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ ( 𝑅1 “ ω ) )
15	14	ralrimiva	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) )
16	2 15	jca	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) → ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) )
17		limom	⊢ Lim ω
18		r1filimi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ∧ Lim ω ) → 𝐴 ∈ ∪ ( 𝑅1 “ ω ) )
19	17 18	mp3an3	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ ω ) )
20	16 19	impbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ ω ) ↔ ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) )