Metamath Proof Explorer

Definition df-np

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 , and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995) (New usage is discouraged.)

Ref Expression
Assertion df-np ⊢𝑷=x|∅⊂x∧x⊂𝑸∧∀y∈x∀zz<𝑸y→z∈x∧∃z∈xy<𝑸z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnp class𝑷
1 vx setvarx
2 c0 class∅
3 1 cv setvarx
4 2 3 wpss wff∅⊂x
5 cnq class𝑸
6 3 5 wpss wffx⊂𝑸
7 4 6 wa wff∅⊂x∧x⊂𝑸
8 vy setvary
9 vz setvarz
10 9 cv setvarz
11 cltq class<𝑸
12 8 cv setvary
13 10 12 11 wbr wffz<𝑸y
14 10 3 wcel wffz∈x
15 13 14 wi wffz<𝑸y→z∈x
16 15 9 wal wff∀zz<𝑸y→z∈x
17 12 10 11 wbr wffy<𝑸z
18 17 9 3 wrex wff∃z∈xy<𝑸z
19 16 18 wa wff∀zz<𝑸y→z∈x∧∃z∈xy<𝑸z
20 19 8 3 wral wff∀y∈x∀zz<𝑸y→z∈x∧∃z∈xy<𝑸z
21 7 20 wa wff∅⊂x∧x⊂𝑸∧∀y∈x∀zz<𝑸y→z∈x∧∃z∈xy<𝑸z
22 21 1 cab classx|∅⊂x∧x⊂𝑸∧∀y∈x∀zz<𝑸y→z∈x∧∃z∈xy<𝑸z
23 0 22 wceq wff𝑷=x|∅⊂x∧x⊂𝑸∧∀y∈x∀zz<𝑸y→z∈x∧∃z∈xy<𝑸z