Theorem hfadj

Description: Adjoining one hereditarily finite set to a hereditarily finite set results in a hereditarily finite set. (Contributed by Scott Fenton, 15-Jul-2015)

	Ref	Expression
Assertion	hfadj	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ { 𝐵 } ) ∈ HF )

Proof

Step	Hyp	Ref	Expression
1		hfsn	⊢ ( 𝐵 ∈ HF → { 𝐵 } ∈ HF )
2		hfun	⊢ ( ( 𝐴 ∈ HF ∧ { 𝐵 } ∈ HF ) → ( 𝐴 ∪ { 𝐵 } ) ∈ HF )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( 𝐴 ∪ { 𝐵 } ) ∈ HF )