This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	\|- -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