MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pnf Structured version   Unicode version

Definition df-pnf 9122
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 9123). 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 9127, mnfnre 9128, and pnfnemnf 10717.

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.)

Assertion
Ref Expression
df-pnf  |-  +oo  =  ~P U. CC

Detailed syntax breakdown of Definition df-pnf
StepHypRef Expression
1 cpnf 9117 . 2  class  +oo
2 cc 8988 . . . 4  class  CC
32cuni 4015 . . 3  class  U. CC
43cpw 3799 . 2  class  ~P U. CC
51, 4wceq 1652 1  wff  +oo  =  ~P U. CC
Colors of variables: wff set class
This definition is referenced by:  pnfnre  9127  mnfnre  9128  pnfxr  10713
  Copyright terms: Public domain W3C validator