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	Could not format assertion : No typesetting found for |- ( A e. HF -> U. A e. HF ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elhf3	Could not format ( A e. HF <-> ( A e. Fin /\ A C_ HF ) ) : No typesetting found for |- ( A e. HF <-> ( A e. Fin /\ A C_ HF ) ) with typecode |-
2		hffi	Could not format ( x e. HF -> x e. Fin ) : No typesetting found for |- ( x e. HF -> x e. Fin ) with typecode |-
3	2	ssriv	Could not format HF C_ Fin : No typesetting found for |- HF C_ Fin with typecode |-
4		sstr	Could not format ( ( A C_ HF /\ HF C_ Fin ) -> A C_ Fin ) : No typesetting found for |- ( ( A C_ HF /\ HF C_ Fin ) -> A C_ Fin ) with typecode |-
5	3 4	mpan2	Could not format ( A C_ HF -> A C_ Fin ) : No typesetting found for |- ( A C_ HF -> A C_ Fin ) with typecode |-
6	5	anim2i	Could not format ( ( A e. Fin /\ A C_ HF ) -> ( A e. Fin /\ A C_ Fin ) ) : No typesetting found for |- ( ( A e. Fin /\ A C_ HF ) -> ( A e. Fin /\ A C_ Fin ) ) with typecode |-
7	1 6	sylbi	Could not format ( A e. HF -> ( A e. Fin /\ A C_ Fin ) ) : No typesetting found for |- ( A e. HF -> ( A e. Fin /\ A C_ Fin ) ) with typecode |-
8		unifi	$$⊢\left(A\in \mathrm{Fin}\wedge A\subseteq \mathrm{Fin}\right)\to \bigcup A\in \mathrm{Fin}$$
9	7 8	syl	Could not format ( A e. HF -> U. A e. Fin ) : No typesetting found for |- ( A e. HF -> U. A e. Fin ) with typecode |-
10		hfelhf	Could not format ( ( y e. A /\ A e. HF ) -> y e. HF ) : No typesetting found for |- ( ( y e. A /\ A e. HF ) -> y e. HF ) with typecode |-
11		elhf3	Could not format ( y e. HF <-> ( y e. Fin /\ y C_ HF ) ) : No typesetting found for |- ( y e. HF <-> ( y e. Fin /\ y C_ HF ) ) with typecode |-
12	11	simprbi	Could not format ( y e. HF -> y C_ HF ) : No typesetting found for |- ( y e. HF -> y C_ HF ) with typecode |-
13	10 12	syl	Could not format ( ( y e. A /\ A e. HF ) -> y C_ HF ) : No typesetting found for |- ( ( y e. A /\ A e. HF ) -> y C_ HF ) with typecode |-
14	13	ancoms	Could not format ( ( A e. HF /\ y e. A ) -> y C_ HF ) : No typesetting found for |- ( ( A e. HF /\ y e. A ) -> y C_ HF ) with typecode |-
15	14	ralrimiva	Could not format ( A e. HF -> A. y e. A y C_ HF ) : No typesetting found for |- ( A e. HF -> A. y e. A y C_ HF ) with typecode |-
16		unissb	Could not format ( U. A C_ HF <-> A. y e. A y C_ HF ) : No typesetting found for |- ( U. A C_ HF <-> A. y e. A y C_ HF ) with typecode |-
17	15 16	sylibr	Could not format ( A e. HF -> U. A C_ HF ) : No typesetting found for |- ( A e. HF -> U. A C_ HF ) with typecode |-
18		elhf3	Could not format ( U. A e. HF <-> ( U. A e. Fin /\ U. A C_ HF ) ) : No typesetting found for |- ( U. A e. HF <-> ( U. A e. Fin /\ U. A C_ HF ) ) with typecode |-
19	9 17 18	sylanbrc	Could not format ( A e. HF -> U. A e. HF ) : No typesetting found for |- ( A e. HF -> U. A e. HF ) with typecode |-