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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpnf
 |-  +oo
1 cc
 |-  CC
2 1 cuni
 |-  U. CC
3 2 cpw
 |-  ~P U. CC
4 0 3 wceq
 |-  +oo = ~P U. CC