Theorem hfun

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

	Ref	Expression
Assertion	hfun	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ 𝐵 ) ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		hffi	⊢ ( 𝐴 ∈ HF → 𝐴 ∈ Fin )
2		hffi	⊢ ( 𝐵 ∈ HF → 𝐵 ∈ Fin )
3		unfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ 𝐵 ) ∈ Fin )
5		elhf3	⊢ ( 𝐴 ∈ HF ↔ ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ HF ) )
6	5	simprbi	⊢ ( 𝐴 ∈ HF → 𝐴 ⊆ HF )
7		elhf3	⊢ ( 𝐵 ∈ HF ↔ ( 𝐵 ∈ Fin ∧ 𝐵 ⊆ HF ) )
8	7	simprbi	⊢ ( 𝐵 ∈ HF → 𝐵 ⊆ HF )
9		unss	⊢ ( ( 𝐴 ⊆ HF ∧ 𝐵 ⊆ HF ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ HF )
10	9	biimpi	⊢ ( ( 𝐴 ⊆ HF ∧ 𝐵 ⊆ HF ) → ( 𝐴 ∪ 𝐵 ) ⊆ HF )
11	6 8 10	syl2an	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ 𝐵 ) ⊆ HF )
12		elhf3	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ HF ↔ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin ∧ ( 𝐴 ∪ 𝐵 ) ⊆ HF ) )
13	4 11 12	sylanbrc	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ 𝐵 ) ∈ HF )