Add nninff to mathbox
Add nninff to mathbox

This is an easy consequence of df-nninf but is used enough times that it
is worth making it a theorem.

Use it in nnsf and nnsf1 .

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