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	⊢ -∞
1		cpnf	⊢ +∞
2	1	cpw	⊢ 𝒫 +∞
3	0 2	wceq	⊢ -∞ = 𝒫 +∞