Add peano5uzi and peano5uzti to iset.mm
Add peano5uzi and peano5uzti to iset.mm

The proof is essentially the same as in set.mm except that set.mm
proves peano5uzi first and then uses dedth to derive peano5uzti .
Since iset.mm doesn't have dedth , we prove peano5uzti first
(carrying along the N e. ZZ condition throughout the proof
but otherwise closely following the set.mm proof of peano5uzi )
and then derive peano5uzi using ax-mp .

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