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

Proof

Step	Hyp	Ref	Expression
1		hffi	Could not format ( A e. HF -> A e. Fin ) : No typesetting found for |- ( A e. HF -> A e. Fin ) with typecode |-
2		hffi	Could not format ( B e. HF -> B e. Fin ) : No typesetting found for |- ( B e. HF -> B e. Fin ) with typecode |-
3		unfi	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\cup B\in \mathrm{Fin}$$
4	1 2 3	syl2an	Could not format ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. Fin ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. Fin ) with typecode |-
5		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 |-
6	5	simprbi	Could not format ( A e. HF -> A C_ HF ) : No typesetting found for |- ( A e. HF -> A C_ HF ) with typecode |-
7		elhf3	Could not format ( B e. HF <-> ( B e. Fin /\ B C_ HF ) ) : No typesetting found for |- ( B e. HF <-> ( B e. Fin /\ B C_ HF ) ) with typecode |-
8	7	simprbi	Could not format ( B e. HF -> B C_ HF ) : No typesetting found for |- ( B e. HF -> B C_ HF ) with typecode |-
9		unss	Could not format ( ( A C_ HF /\ B C_ HF ) <-> ( A u. B ) C_ HF ) : No typesetting found for |- ( ( A C_ HF /\ B C_ HF ) <-> ( A u. B ) C_ HF ) with typecode |-
10	9	biimpi	Could not format ( ( A C_ HF /\ B C_ HF ) -> ( A u. B ) C_ HF ) : No typesetting found for |- ( ( A C_ HF /\ B C_ HF ) -> ( A u. B ) C_ HF ) with typecode |-
11	6 8 10	syl2an	Could not format ( ( A e. HF /\ B e. HF ) -> ( A u. B ) C_ HF ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) C_ HF ) with typecode |-
12		elhf3	Could not format ( ( A u. B ) e. HF <-> ( ( A u. B ) e. Fin /\ ( A u. B ) C_ HF ) ) : No typesetting found for |- ( ( A u. B ) e. HF <-> ( ( A u. B ) e. Fin /\ ( A u. B ) C_ HF ) ) with typecode |-
13	4 11 12	sylanbrc	Could not format ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A u. B ) e. HF ) with typecode |-