Theorem r1omtsk

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)

	Ref	Expression
Assertion	r1omtsk	$$⊢R_1\left(\mathrm{\omega }\right)\in \mathrm{Tarski}$$

Proof

Step	Hyp	Ref	Expression
1		omina	$$⊢\mathrm{\omega }\in \mathrm{Inacc}$$
2		inatsk	$$⊢\mathrm{\omega }\in \mathrm{Inacc}\to R_1\left(\mathrm{\omega }\right)\in \mathrm{Tarski}$$
3	1 2	ax-mp	$$⊢R_1\left(\mathrm{\omega }\right)\in \mathrm{Tarski}$$