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	|- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF )

Proof

Step	Hyp	Ref	Expression
1		hffi	|- ( A e. HF -> A e. Fin )
2		hffi	|- ( B e. HF -> B e. Fin )
3		unfi	|- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
4	1 2 3	syl2an	|- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. Fin )
5		elhf3	|- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) )
6	5	simprbi	|- ( A e. HF -> A C_ HF )
7		elhf3	|- ( B e. HF <-> ( B e. Fin /\ B C_ HF ) )
8	7	simprbi	|- ( B e. HF -> B C_ HF )
9		unss	|- ( ( A C_ HF /\ B C_ HF ) <-> ( A u. B ) C_ HF )
10	9	biimpi	|- ( ( A C_ HF /\ B C_ HF ) -> ( A u. B ) C_ HF )
11	6 8 10	syl2an	|- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) C_ HF )
12		elhf3	|- ( ( A u. B ) e. HF <-> ( ( A u. B ) e. Fin /\ ( A u. B ) C_ HF ) )
13	4 11 12	sylanbrc	|- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF )