Definition df-np 10397

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 10537, 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 = {𝑥 ∣ ((∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q) ∧ ∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧))}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-np

Step	Hyp	Ref	Expression
1		cnp 10275	. 2 class P
2		c0 4290	. . . . . 6 class ∅
3		vx	. . . . . . 7 setvar 𝑥
4	3	cv 1532	. . . . . 6 class 𝑥
5	2, 4	wpss 3936	. . . . 5 wff ∅ ⊊ 𝑥
6		cnq 10268	. . . . . 6 class Q
7	4, 6	wpss 3936	. . . . 5 wff 𝑥 ⊊ Q
8	5, 7	wa 398	. . . 4 wff (∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q)
9		vz	. . . . . . . . . 10 setvar 𝑧
10	9	cv 1532	. . . . . . . . 9 class 𝑧
11		vy	. . . . . . . . . 10 setvar 𝑦
12	11	cv 1532	. . . . . . . . 9 class 𝑦
13		cltq 10274	. . . . . . . . 9 class <Q
14	10, 12, 13	wbr 5058	. . . . . . . 8 wff 𝑧 <Q 𝑦
15	9, 3	wel 2111	. . . . . . . 8 wff 𝑧 ∈ 𝑥
16	14, 15	wi 4	. . . . . . 7 wff (𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥)
17	16, 9	wal 1531	. . . . . 6 wff ∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥)
18	12, 10, 13	wbr 5058	. . . . . . 7 wff 𝑦 <Q 𝑧
19	18, 9, 4	wrex 3139	. . . . . 6 wff ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧
20	17, 19	wa 398	. . . . 5 wff (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧)
21	20, 11, 4	wral 3138	. . . 4 wff ∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧)
22	8, 21	wa 398	. . 3 wff ((∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q) ∧ ∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧))
23	22, 3	cab 2799	. 2 class {𝑥 ∣ ((∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q) ∧ ∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧))}
24	1, 23	wceq 1533	1 wff P = {𝑥 ∣ ((∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q) ∧ ∀𝑦 ∈ 𝑥 (∀𝑧(𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥) ∧ ∃𝑧 ∈ 𝑥 𝑦 <Q 𝑧))}

This definition is referenced by:  npex  10402  elnp  10403  elnpi  10404