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 10738
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 10878, 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 10616 . 2 class P
2 c0 4262 . . . . . 6 class
3 vx . . . . . . 7 setvar 𝑥
43cv 1541 . . . . . 6 class 𝑥
52, 4wpss 3893 . . . . 5 wff ∅ ⊊ 𝑥
6 cnq 10609 . . . . . 6 class Q
74, 6wpss 3893 . . . . 5 wff 𝑥Q
85, 7wa 396 . . . 4 wff (∅ ⊊ 𝑥𝑥Q)
9 vz . . . . . . . . . 10 setvar 𝑧
109cv 1541 . . . . . . . . 9 class 𝑧
11 vy . . . . . . . . . 10 setvar 𝑦
1211cv 1541 . . . . . . . . 9 class 𝑦
13 cltq 10615 . . . . . . . . 9 class <Q
1410, 12, 13wbr 5079 . . . . . . . 8 wff 𝑧 <Q 𝑦
159, 3wel 2111 . . . . . . . 8 wff 𝑧𝑥
1614, 15wi 4 . . . . . . 7 wff (𝑧 <Q 𝑦𝑧𝑥)
1716, 9wal 1540 . . . . . 6 wff 𝑧(𝑧 <Q 𝑦𝑧𝑥)
1812, 10, 13wbr 5079 . . . . . . 7 wff 𝑦 <Q 𝑧
1918, 9, 4wrex 3067 . . . . . 6 wff 𝑧𝑥 𝑦 <Q 𝑧
2017, 19wa 396 . . . . 5 wff (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧)
2120, 11, 4wral 3066 . . . 4 wff 𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧)
228, 21wa 396 . . 3 wff ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))
2322, 3cab 2717 . 2 class {𝑥 ∣ ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))}
241, 23wceq 1542 1 wff P = {𝑥 ∣ ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  npex  10743  elnp  10744  elnpi  10745
  Copyright terms: Public domain W3C validator