Add tfrlemi1 to iset.mm
Add tfrlemi1 to iset.mm

This is a lemma for transfinite recursion and is a step towards
saying that when we define a function via recursion, it is
defined on all ordinals.

It includes the following lemmas: tfrlemifvex ,
tfrlemisucfn , tfrlemisucacc , tfrlemibacc , tfrlem5-2 ,
tfrlemibfun , tfrlemiex , tfrlemibex , tfrlemibdmx ,
tfrlemibxssdm , tfrlem3-2 , tfrlemiubacc.

Move tfrlem2a earlier in the file.

Add distinct variable constraint between f A and f B, seems like
it may be easier to do the variable change at the end rather than
throughout the proofs.

Move tfrlemi14 later, rename from tfrlem14 , and add hypothesis

metamath/set.mm,metamath/set.mm,metamath/set.mm