Metamath Proof Explorer


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 +∞ = 𝒫