Metamath Proof Explorer

Definition df-mnf

Description: Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that -oo be a set not in RR and different from +oo (see mnfnre and pnfnemnf ). (Contributed by NM, 13-Oct-2005) (New usage is discouraged.)

Ref Expression
Assertion df-mnf −∞ = 𝒫 +∞

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmnf class −∞
1 cpnf class +∞
2 1 cpw class 𝒫 +∞
3 0 2 wceq wff −∞ = 𝒫 +∞