This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∀ z z < 𝑸 y → z ∈ x ∧ ∃ z ∈ x y < 𝑸 z

Detailed syntax breakdown

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