Definition df-pnf 5684

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 5685). 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 5693, mnfnre 5694, and pnfnemnf 5733.

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 5680	. 2 class +oo
2		cc 5429	. . . 4 class CC
3	2	cuni 2608	. . 3 class U.CC
4	3	cpw 2495	. 2 class P~U.CC
5	1, 4	wceq 1018	1 wff +oo = P~U.CC

This definition is referenced by:  pnfxr 5690  mnfxr 5691  pnfnre 5693  mnfnre 5694

Copyright terms: Public domain