HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-pnf 6846
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 6847). We use ~PU.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 6855, mnfnre 6856, and pnfnemnf 6895.

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.

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

Detailed syntax breakdown of Definition df-pnf
StepHypRef Expression
1 cpnf 6842 . 2 class +oo
2 cc 6750 . . . 4 class CC
32cuni 3366 . . 3 class U.CC
43cpw 3227 . 2 class ~PU.CC
51, 4wceq 1586 1 wff +oo = ~PU.CC
Colors of variables: wff set class
This definition is referenced by:  pnfxr 6852  pnfnre 6855  mnfnre 6856
Copyright terms: Public domain