Description: Define plus infinity.
Note that the definition is arbitrary, requiring
only that be a set not in
and different from
(df-mnf9300). We use to make it independent of the
construction of , and Cantor's
Theorem will show that it is
different from any member of and therefore . See pnfnre9304,
mnfnre9305, and pnfnemnf10961.
A simpler possibility is to define as and as
, but that approach requires the Axiom of Regularity to show
that and are different from each other
and from all
members of . (Contributed by
NM, 13-Oct-2005.)
(New usage is discouraged.)
