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 | ⊢ +∞ = 𝒫 ∪ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cpnf | ⊢ +∞ | |
1 | cc | ⊢ ℂ | |
2 | 1 | cuni | ⊢ ∪ ℂ |
3 | 2 | cpw | ⊢ 𝒫 ∪ ℂ |
4 | 0 3 | wceq | ⊢ +∞ = 𝒫 ∪ ℂ |