Definition df-np 5086

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 5240, and is intended to be used only by the construction.)

Assertion

Ref	Expression
df-np	|- P. = {x | (((/) (. x /\ x (. 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 4985	. 2 class P.
2		c0 2280	. . . . . 6 class (/)
3		vx	. . . . . . 7 set x
4	3	cv 955	. . . . . 6 class x
5	2, 4	wpss 2048	. . . . 5 wff (/) (. x
6		cnq 4979	. . . . . 6 class Q.
7	4, 6	wpss 2048	. . . . 5 wff x (. Q.
8	5, 7	wa 223	. . . 4 wff ((/) (. x /\ x (. Q.)
9		vz	. . . . . . . . . 10 set z
10	9	cv 955	. . . . . . . . 9 class z
11		vy	. . . . . . . . . 10 set y
12	11	cv 955	. . . . . . . . 9 class y
13		cltq 4984	. . . . . . . . 9 class <Q
14	10, 12, 13	wbr 2619	. . . . . . . 8 wff z <Q y
15	10, 4	wcel 958	. . . . . . . 8 wff z e. x
16	14, 15	wi 3	. . . . . . 7 wff (z <Q y -> z e. x)
17	16, 9	wal 954	. . . . . 6 wff A.z(z <Q y -> z e. x)
18	12, 10, 13	wbr 2619	. . . . . . 7 wff y <Q z
19	18, 9, 4	wrex 1646	. . . . . 6 wff E.z e. x y <Q z
20	17, 19	wa 223	. . . . 5 wff (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z)
21	20, 11, 4	wral 1645	. . . 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 223	. . 3 wff (((/) (. x /\ x (. Q.) /\ A.y e. x (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z))
23	22, 3	cab 1463	. 2 class {x | (((/) (. x /\ x (. Q.) /\ A.y e. x (A.z(z <Q y -> z e. x) /\ E.z e. x y <Q z))}
24	1, 23	wceq 956	1 wff P. = {x | (((/) (. x /\ x (. 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 5091  elnp 5092

Copyright terms: Public domain