Theorem hftsk

Description: The set of hereditarily finite sets is a Tarski class. (The Tarski-Grothendieck Axiom is not needed for this theorem.) (Contributed by Mario Carneiro, 28-May-2013) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026)

	Ref	Expression
Assertion	hftsk	⊢ HF ∈ Tarski

Proof

Step	Hyp	Ref	Expression
1		dfhf2	⊢ HF = ( 𝑅1 ‘ ω )
2		omina	⊢ ω ∈ Inacc
3		inatsk	⊢ ( ω ∈ Inacc → ( 𝑅1 ‘ ω ) ∈ Tarski )
4	2 3	ax-mp	⊢ ( 𝑅1 ‘ ω ) ∈ Tarski
5	1 4	eqeltri	⊢ HF ∈ Tarski