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 P = { 𝑥 ∣ ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnp ⊢ P
1 vx ⊢ 𝑥
2 c0 ⊢ ∅
3 1 cv ⊢ 𝑥
4 2 3 wpss ⊢ ∅ ⊊ 𝑥
5 cnq ⊢ Q
6 3 5 wpss ⊢ 𝑥 ⊊ Q
7 4 6 wa ⊢ ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q )
8 vy ⊢ 𝑦
9 vz ⊢ 𝑧
10 9 cv ⊢ 𝑧
11 cltq ⊢ <Q
12 8 cv ⊢ 𝑦
13 10 12 11 wbr ⊢ 𝑧 <Q 𝑦
14 10 3 wcel ⊢ 𝑧 ∈ 𝑥
15 13 14 wi ⊢ ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 )
16 15 9 wal ⊢ ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 )
17 12 10 11 wbr ⊢ 𝑦 <Q 𝑧
18 17 9 3 wrex ⊢ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧
19 16 18 wa ⊢ ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 )
20 19 8 3 wral ⊢ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 )
21 7 20 wa ⊢ ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) )
22 21 1 cab ⊢ { 𝑥 ∣ ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) ) }
23 0 22 wceq ⊢ P = { 𝑥 ∣ ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) ) }