Add disjnim to iset.mm
Add disjnim to iset.mm

This is in part taken from disjor in set.mm and the proof uses
some of the steps. The changes are to change disjunction to
negation and implication, and to only keep one direction of
the biconditional.

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