Theorem hfuni

Description: The union of a hereditarily finite set is hereditarily finite. (Contributed by Scott Fenton, 16-Jul-2015) Avoid ax-reg , ax-inf2 . (Revised by BTernaryTau, 17-Sep-2026)

	Ref	Expression
Assertion	hfuni	⊢ ( 𝐴 ∈ HF → ∪ 𝐴 ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		elhf3	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) )
2		hffi	⊢ ( 𝑥 ∈ HF → 𝑥 ∈ Fin )
3	2	ssriv	⊢ HF ⊆ Fin
4		sstr	⊢ ( ( 𝐴 ⊆ HF ∧ HF ⊆ Fin ) → 𝐴 ⊆ Fin )
5	3 4	mpan2	⊢ ( 𝐴 ⊆ HF → 𝐴 ⊆ Fin )
6	5	anim2i	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) → ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) )
7	1 6	sylbi	⊢ ( 𝐴 ∈ HF → ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) )
8		unifi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin ) → ∪ 𝐴 ∈ Fin )
9	7 8	syl	⊢ ( 𝐴 ∈ HF → ∪ 𝐴 ∈ Fin )
10		hfelhf	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝐴 ∈ HF ) → 𝑦 ∈ HF )
11		elhf3	⊢ ( 𝑦 ∈ HF ↔ ( 𝑦 ∈ Fin ∧ 𝑦 ⊆ HF ) )
12	11	simprbi	⊢ ( 𝑦 ∈ HF → 𝑦 ⊆ HF )
13	10 12	syl	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝐴 ∈ HF ) → 𝑦 ⊆ HF )
14	13	ancoms	⊢ ( ( 𝐴 ∈ HF ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ HF )
15	14	ralrimiva	⊢ ( 𝐴 ∈ HF → ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ HF )
16		unissb	⊢ ( ∪ 𝐴 ⊆ HF ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ⊆ HF )
17	15 16	sylibr	⊢ ( 𝐴 ∈ HF → ∪ 𝐴 ⊆ HF )
18		elhf3	⊢ ( ∪ 𝐴 ∈ HF ↔ ( ∪ 𝐴 ∈ Fin ∧ ∪ 𝐴 ⊆ HF ) )
19	9 17 18	sylanbrc	⊢ ( 𝐴 ∈ HF → ∪ 𝐴 ∈ HF )