Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-np Structured version   Visualization version   GIF version

Definition df-np 10004
 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 10143, 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
StepHypRef Expression
1 cnp 9882 . 2 class P
2 c0 4061 . . . . . 6 class
3 vx . . . . . . 7 setvar 𝑥
43cv 1629 . . . . . 6 class 𝑥
52, 4wpss 3722 . . . . 5 wff ∅ ⊊ 𝑥
6 cnq 9875 . . . . . 6 class Q
74, 6wpss 3722 . . . . 5 wff 𝑥Q
85, 7wa 382 . . . 4 wff (∅ ⊊ 𝑥𝑥Q)
9 vz . . . . . . . . . 10 setvar 𝑧
109cv 1629 . . . . . . . . 9 class 𝑧
11 vy . . . . . . . . . 10 setvar 𝑦
1211cv 1629 . . . . . . . . 9 class 𝑦
13 cltq 9881 . . . . . . . . 9 class <Q
1410, 12, 13wbr 4784 . . . . . . . 8 wff 𝑧 <Q 𝑦
159, 3wel 2145 . . . . . . . 8 wff 𝑧𝑥
1614, 15wi 4 . . . . . . 7 wff (𝑧 <Q 𝑦𝑧𝑥)
1716, 9wal 1628 . . . . . 6 wff 𝑧(𝑧 <Q 𝑦𝑧𝑥)
1812, 10, 13wbr 4784 . . . . . . 7 wff 𝑦 <Q 𝑧
1918, 9, 4wrex 3061 . . . . . 6 wff 𝑧𝑥 𝑦 <Q 𝑧
2017, 19wa 382 . . . . 5 wff (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧)
2120, 11, 4wral 3060 . . . 4 wff 𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧)
228, 21wa 382 . . 3 wff ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))
2322, 3cab 2756 . 2 class {𝑥 ∣ ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))}
241, 23wceq 1630 1 wff P = {𝑥 ∣ ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))}
 Colors of variables: wff setvar class This definition is referenced by:  npex  10009  elnp  10010  elnpi  10011
 Copyright terms: Public domain W3C validator