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

Proof

Step	Hyp	Ref	Expression
1		dfhf2	Could not format HF = ( R1 ` _om ) : No typesetting found for |- HF = ( R1 ` _om ) with typecode |-
2		omina	$$⊢\mathrm{\omega }\in \mathrm{Inacc}$$
3		inatsk	$$⊢\mathrm{\omega }\in \mathrm{Inacc}\to R_1\left(\mathrm{\omega }\right)\in \mathrm{Tarski}$$
4	2 3	ax-mp	$$⊢R_1\left(\mathrm{\omega }\right)\in \mathrm{Tarski}$$
5	1 4	eqeltri	Could not format HF e. Tarski : No typesetting found for |- HF e. Tarski with typecode |-