Theorem elhf4

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

	Ref	Expression
Assertion	elhf4	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ HF ) )

Proof

Step	Hyp	Ref	Expression
1		hffi	⊢ ( 𝐴 ∈ HF → 𝐴 ∈ Fin )
2		r1tr	⊢ Tr ( 𝑅1 ‘ 𝑦 )
3		trel	⊢ ( Tr ( 𝑅1 ‘ 𝑦 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
4	2 3	ax-mp	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
5	4	ex	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
6	5	reximdv	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) → ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) ) )
7		elhf	⊢ ( 𝐴 ∈ HF ↔ ∃ 𝑦 ∈ ω 𝐴 ∈ ( 𝑅1 ‘ 𝑦 ) )
8		elhf	⊢ ( 𝑥 ∈ HF ↔ ∃ 𝑦 ∈ ω 𝑥 ∈ ( 𝑅1 ‘ 𝑦 ) )
9	6 7 8	3imtr4g	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ HF → 𝑥 ∈ HF ) )
10	9	com12	⊢ ( 𝐴 ∈ HF → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ HF ) )
11	10	ralrimiv	⊢ ( 𝐴 ∈ HF → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ HF )
12	1 11	jca	⊢ ( 𝐴 ∈ HF → ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ HF ) )
13		df-hf	⊢ HF = ∪ ( 𝑅1 “ ω )
14	13	eleq2i	⊢ ( 𝑥 ∈ HF ↔ 𝑥 ∈ ∪ ( 𝑅1 “ ω ) )
15	14	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ HF ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) )
16		limom	⊢ Lim ω
17		r1filimi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ∧ Lim ω ) → 𝐴 ∈ ∪ ( 𝑅1 “ ω ) )
18	16 17	mp3an3	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ ω ) )
19	18 13	eleqtrrdi	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) → 𝐴 ∈ HF )
20	15 19	sylan2b	⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ HF ) → 𝐴 ∈ HF )
21	12 20	impbii	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ HF ) )