Definition df-pnf 5467

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 5468). 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 5476, mnfnre 5477, and pnfnemnf 5517.

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

Detailed syntax breakdown of Definition df-pnf

Step	Hyp	Ref	Expression
1		cpnf 5463	. 2 class +oo
2		cc 5212	. . . 4 class CC
3	2	cuni 2498	. . 3 class U.CC
4	3	cpw 2397	. 2 class P~U.CC
5	1, 4	wceq 954	1 wff +oo = P~U.CC

This definition is referenced by:  pnfxr 5473  mnfxr 5474  pnfnre 5476  mnfnre 5477  pnfnemnf 5517

Copyright terms: Public domain