Hereditarily finite sets

[Eric Schmidt]

The class of hereditarily finite sets may be defined as U. ( R1 " _om ). Assuming Infinity, we have the simpler expression ( R1 ` _om ). There are a few theorems about this class in the main part of set.mm. There are more in the mathboxes of BTernaryTau and Scott Fenton. Fenton's mathbox introduces the definition df-hf $a |- Hf = U. ( R1 " _om ).

Some work I am planning will probably use some of the results from Fenton's mathbox. This would seem to require moving df-hf to main. Would this be considered acceptable?

List of all statements in set.mm about herdditarily finite sets:

Main:

37768 ackbij2 $p |- H : U. ( R1 " _om ) -1-1-onto-> _om [H is defined in the hypotheses]
37772 r1om $p |- ( R1 ` _om ) ~~ _om
39510 tskr1om2 $p |- ( ( T e. Tarski /\ T =/= (/) ) -> U. ( R1 " _om ) C_ T )
39533 r1omALT $p |- ( R1 ` _om ) ~~ _om
39542 r1omtsk $p |- ( R1 ` _om ) e. Tarski

BTernaryTau's mathbox:

157193 r1omfi $p |- U. ( R1 " _om ) C_ Fin
157197 r1omhf $p |- ( A e. U. ( R1 " _om ) <-> ( A e. Fin /\ A. x e. A x e. U.
    ( R1 " _om ) ) )
157211 r1omfv $p |- ( R1 ` _om ) = U. ( R1 " _om )
157214 trssfir1om $p |- ( ( Tr A /\ A C_ Fin ) -> A C_ U. ( R1 " _om ) )
157218 r1omhfb $p |- ( H = U. ( R1 " _om ) <-> A. x ( x e. H <-> ( x e. Fin /\
    A. y e. x y e. H ) ) )
157339 trssfir1omregs $p |- ( ( Tr A /\ A C_ Fin ) -> A C_ U. ( R1 " _om ) )
157343 r1omhfbregs $p |- ( H = U. ( R1 " _om ) <-> A. x ( x e. H <-> ( x e. Fin
    /\ A. y e. x y e. H ) ) )
157345 fineqvr1ombregs $p |- ( Fin = _V <-> U. ( R1 " _om ) = _V )

Scott Fenton's mathbox:

162283 chf $a class Hf
162284 df-hf $a |- Hf = U. ( R1 " _om )
162287 elhf $p |- ( A e. Hf <-> E. x e. _om A e. ( R1 ` x ) )
162292 elhf2 $p |- ( A e. Hf <-> ( rank ` A ) e. _om )
162296 elhf2g $p |- ( A e. V -> ( A e. Hf <-> ( rank ` A ) e. _om ) )
162298 0hf $p |- (/) e. Hf
162299 hfun $p |- ( ( A e. Hf /\ B e. Hf ) -> ( A u. B ) e. Hf )
162300 hfsn $p |- ( A e. Hf -> { A } e. Hf )
162301 hfadj $p |- ( ( A e. Hf /\ B e. Hf ) -> ( A u. { B } ) e. Hf )
162302 hfelhf $p |- ( ( A e. B /\ B e. Hf ) -> A e. Hf )
162305 hftr $p |- Tr Hf
162310 hfext $p |- ( ( A e. Hf /\ B e. Hf ) -> ( A = B <-> A. x e. Hf ( x e. A
    <-> x e. B ) ) )
162312 hfuni $p |- ( A e. Hf -> U. A e. Hf )
162313 hfpw $p |- ( A e. Hf -> ~P A e. Hf )
162314 hfninf $p |- -. _om e. Hf

Also, I should mention a couple of theorems that refer to ( R1 " _om ) without taking the union:

39402 wunr1om $e |- ( ph -> U e. WUni ) $. $p |- ( ph -> ( R1 " _om ) C_ U )
39509 tskr1om $p |- ( ( T e. Tarski /\ T =/= (/) ) -> ( R1 " _om ) C_ T )

[Thierry Arnoux]

Hi Eric,

Yes, sure, feel free to write a PR which moves the definition of hereditarily finite sets to the main part of set.mm, and any other theorem you need from other people's mathboxes.
This could probably go after chapter 2.6.9, "Rank".

BR,
_
Thierry

On 21/07/2026 07:16, Eric Schmidt wrote:

The class of hereditarily finite sets may be defined as U. ( R1 " _om ). Assuming Infinity, we have the simpler expression ( R1 ` _om ). There are a few theorems about this class in the main part of set.mm. There are more in the mathboxes of BTernaryTau and Scott Fenton. Fenton's mathbox introduces the definition df-hf $a |- Hf = U. ( R1 " _om ).

Some work I am planning will probably use some of the results from Fenton's mathbox. This would seem to require moving df-hf to main. Would this be considered acceptable?

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/a004fa49-30bb-4aa7-afc0-589765f383dan%40googlegroups.com.