Definition df-pnf

Description: Define plus infinity. Note that the definition is arbitrary, requiring only that +oo be a set not in RR and different from -oo ( df-mnf ). We use ~P U. CC to make it independent of the construction of CC , and Cantor's Theorem will show that it is different from any member of CC and therefore RR . See pnfnre , mnfnre , and pnfnemnf .

A simpler possibility is to define +oo as CC and -oo as { CC } , but that approach requires the Axiom of Regularity to show that +oo and -oo are different from each other and from all members of RR . (Contributed by NM, 13-Oct-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	df-pnf	⊢ +∞ = 𝒫 ∪ ℂ

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpnf	⊢ +∞
1		cc	⊢ ℂ
2	1	cuni	⊢ ∪ ℂ
3	2	cpw	⊢ 𝒫 ∪ ℂ
4	0 3	wceq	⊢ +∞ = 𝒫 ∪ ℂ