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 𝑧 ) ) }