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	$$⊢\mathrm{-\infty }=𝒫\mathrm{+\infty }$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmnf	$$class\mathrm{-\infty }$$
1		cpnf	$$class\mathrm{+\infty }$$
2	1	cpw	$$class𝒫\mathrm{+\infty }$$
3	0 2	wceq	$$wff\mathrm{-\infty }=𝒫\mathrm{+\infty }$$