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	|- -oo = ~P +oo

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmnf	|- -oo
1		cpnf	|- +oo
2	1	cpw	|- ~P +oo
3	0 2	wceq	|- -oo = ~P +oo