Definition df-np

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 , and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995) (New usage is discouraged.)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnp	|- P.
1		vx	|- x
2		c0	|- (/)
3	1	cv	|- x
4	2 3	wpss	|- (/) C. x
5		cnq	|- Q.
6	3 5	wpss	|- x C. Q.
7	4 6	wa	|- ( (/) C. x /\ x C. Q. )
8		vy	|- y
9		vz	|- z
10	9	cv	|- z
11		cltq	|-
12	8	cv	|- y
13	10 12 11	wbr	|- z
14	10 3	wcel	|- z e. x
15	13 14	wi	|- ( z z e. x )
16	15 9	wal	|- A. z ( z z e. x )
17	12 10 11	wbr	|- y
18	17 9 3	wrex	|- E. z e. x y
19	16 18	wa	|- ( A. z ( z z e. x ) /\ E. z e. x y
20	19 8 3	wral	|- A. y e. x ( A. z ( z z e. x ) /\ E. z e. x y
21	7 20	wa	|- ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z z e. x ) /\ E. z e. x y
22	21 1	cab	|- { x | ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z z e. x ) /\ E. z e. x y
23	0 22	wceq	|- P. = { x | ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z z e. x ) /\ E. z e. x y