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