Definition df-np 9803

Description: Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other. A positive real is defined as the lower class of a Dedekind cut. Definition 9-3.1 of [Gleason] p. 121. (Note: This is a "temporary" definition used in the construction of complex numbers df-c 9942, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
df-np	|- P. = { x | ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z <Q y -> z e. x ) /\ E. z e. x y <Q z ) ) }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-np

Step	Hyp	Ref	Expression
1		cnp 9681	. 2 class P.
2		c0 3915	. . . . . 6 class (/)
3		vx	. . . . . . 7 setvar x
4	3	cv 1482	. . . . . 6 class x
5	2, 4	wpss 3575	. . . . 5 wff (/) C. x
6		cnq 9674	. . . . . 6 class Q.
7	4, 6	wpss 3575	. . . . 5 wff x C. Q.
8	5, 7	wa 384	. . . 4 wff ( (/) C. x /\ x C. Q. )
9		vz	. . . . . . . . . 10 setvar z
10	9	cv 1482	. . . . . . . . 9 class z
11		vy	. . . . . . . . . 10 setvar y
12	11	cv 1482	. . . . . . . . 9 class y
13		cltq 9680	. . . . . . . . 9 class <Q
14	10, 12, 13	wbr 4653	. . . . . . . 8 wff z <Q y
15	9, 3	wel 1991	. . . . . . . 8 wff z e. x
16	14, 15	wi 4	. . . . . . 7 wff ( z <Q y -> z e. x )
17	16, 9	wal 1481	. . . . . 6 wff A. z ( z <Q y -> z e. x )
18	12, 10, 13	wbr 4653	. . . . . . 7 wff y <Q z
19	18, 9, 4	wrex 2913	. . . . . 6 wff E. z e. x y <Q z
20	17, 19	wa 384	. . . . 5 wff ( A. z ( z <Q y -> z e. x ) /\ E. z e. x y <Q z )
21	20, 11, 4	wral 2912	. . . 4 wff A. y e. x ( A. z ( z <Q y -> z e. x ) /\ E. z e. x y <Q z )
22	8, 21	wa 384	. . 3 wff ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z <Q y -> z e. x ) /\ E. z e. x y <Q z ) )
23	22, 3	cab 2608	. 2 class { x | ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z <Q y -> z e. x ) /\ E. z e. x y <Q z ) ) }
24	1, 23	wceq 1483	1 wff P. = { x | ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z <Q y -> z e. x ) /\ E. z e. x y <Q z ) ) }

This definition is referenced by:  npex  9808  elnp  9809  elnpi  9810