Definition df-pnf 5459

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 5460). 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 5468, mnfnre 5469, and pnfnemnf 5509.

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 5455	. 2 class +oo
2		cc 5204	. . . 4 class CC
3	2	cuni 2493	. . 3 class U.CC
4	3	cpw 2391	. 2 class P~U.CC
5	1, 4	wceq 953	1 wff +oo = P~U.CC

This definition is referenced by:  pnfxr 5465  mnfxr 5466  pnfnre 5468  mnfnre 5469  pnfnemnf 5509

Copyright terms: Public domain