Theorem hfadj

Description: Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015)

	Ref	Expression
Assertion	hfadj	$$⊢\left(A\in \mathrm{Hf}\wedge B\in \mathrm{Hf}\right)\to A\cup \left\{B\right\}\in \mathrm{Hf}$$

Proof

Step	Hyp	Ref	Expression
1		hfsn	$$⊢B\in \mathrm{Hf}\to \left\{B\right\}\in \mathrm{Hf}$$
2		hfun	$$⊢\left(A\in \mathrm{Hf}\wedge \left\{B\right\}\in \mathrm{Hf}\right)\to A\cup \left\{B\right\}\in \mathrm{Hf}$$
3	1 2	sylan2	$$⊢\left(A\in \mathrm{Hf}\wedge B\in \mathrm{Hf}\right)\to A\cup \left\{B\right\}\in \mathrm{Hf}$$