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	|- ( A e. HF -> U. A e. HF )

Proof

Step	Hyp	Ref	Expression
1		elhf3	|- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) )
2		hffi	|- ( x e. HF -> x e. Fin )
3	2	ssriv	|- HF C_ Fin
4		sstr	|- ( ( A C_ HF /\ HF C_ Fin ) -> A C_ Fin )
5	3 4	mpan2	|- ( A C_ HF -> A C_ Fin )
6	5	anim2i	|- ( ( A e. Fin /\ A C_ HF ) -> ( A e. Fin /\ A C_ Fin ) )
7	1 6	sylbi	|- ( A e. HF -> ( A e. Fin /\ A C_ Fin ) )
8		unifi	|- ( ( A e. Fin /\ A C_ Fin ) -> U. A e. Fin )
9	7 8	syl	|- ( A e. HF -> U. A e. Fin )
10		hfelhf	|- ( ( y e. A /\ A e. HF ) -> y e. HF )
11		elhf3	|- ( y e. HF <-> ( y e. Fin /\ y C_ HF ) )
12	11	simprbi	|- ( y e. HF -> y C_ HF )
13	10 12	syl	|- ( ( y e. A /\ A e. HF ) -> y C_ HF )
14	13	ancoms	|- ( ( A e. HF /\ y e. A ) -> y C_ HF )
15	14	ralrimiva	|- ( A e. HF -> A. y e. A y C_ HF )
16		unissb	|- ( U. A C_ HF <-> A. y e. A y C_ HF )
17	15 16	sylibr	|- ( A e. HF -> U. A C_ HF )
18		elhf3	|- ( U. A e. HF <-> ( U. A e. Fin /\ U. A C_ HF ) )
19	9 17 18	sylanbrc	|- ( A e. HF -> U. A e. HF )