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 e. Tarski |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfhf2 | |- HF = ( R1 ` _om ) |
|
| 2 | omina | |- _om e. Inacc |
|
| 3 | inatsk | |- ( _om e. Inacc -> ( R1 ` _om ) e. Tarski ) |
|
| 4 | 2 3 | ax-mp | |- ( R1 ` _om ) e. Tarski |
| 5 | 1 4 | eqeltri | |- HF e. Tarski |