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

Definition df-np 9682
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 9821, 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 9560 . 2 class P
2 c0 3874 . . . . . 6 class
3 vx . . . . . . 7 setvar 𝑥
43cv 1474 . . . . . 6 class 𝑥
52, 4wpss 3541 . . . . 5 wff ∅ ⊊ 𝑥
6 cnq 9553 . . . . . 6 class Q
74, 6wpss 3541 . . . . 5 wff 𝑥Q
85, 7wa 383 . . . 4 wff (∅ ⊊ 𝑥𝑥Q)
9 vz . . . . . . . . . 10 setvar 𝑧
109cv 1474 . . . . . . . . 9 class 𝑧
11 vy . . . . . . . . . 10 setvar 𝑦
1211cv 1474 . . . . . . . . 9 class 𝑦
13 cltq 9559 . . . . . . . . 9 class <Q
1410, 12, 13wbr 4583 . . . . . . . 8 wff 𝑧 <Q 𝑦
159, 3wel 1978 . . . . . . . 8 wff 𝑧𝑥
1614, 15wi 4 . . . . . . 7 wff (𝑧 <Q 𝑦𝑧𝑥)
1716, 9wal 1473 . . . . . 6 wff 𝑧(𝑧 <Q 𝑦𝑧𝑥)
1812, 10, 13wbr 4583 . . . . . . 7 wff 𝑦 <Q 𝑧
1918, 9, 4wrex 2897 . . . . . 6 wff 𝑧𝑥 𝑦 <Q 𝑧
2017, 19wa 383 . . . . 5 wff (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧)
2120, 11, 4wral 2896 . . . 4 wff 𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧)
228, 21wa 383 . . 3 wff ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))
2322, 3cab 2596 . 2 class {𝑥 ∣ ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))}
241, 23wceq 1475 1 wff P = {𝑥 ∣ ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  npex  9687  elnp  9688  elnpi  9689
  Copyright terms: Public domain W3C validator