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 )