Definition df-inp 7428

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.

Here we follow the definition of a Dedekind cut from Definition 11.2.1 of [HoTT], p. (varies) with the one exception that we define it over positive rational numbers rather than all rational numbers.

A Dedekind cut is an ordered pair of a lower set 𝑙 and an upper set 𝑢 which is inhabited (∃𝑞 ∈ Q𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q𝑟 ∈ 𝑢), rounded (∀𝑞 ∈ Q(𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q(𝑞 <_Q 𝑟 ∧ 𝑟 ∈ 𝑙)) and likewise for 𝑢), disjoint (∀𝑞 ∈ Q¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢)) and located (∀𝑞 ∈ Q∀𝑟 ∈ Q(𝑞 <_Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))). See HoTT for more discussion of those terms and different ways of defining Dedekind cuts.

(Note: This is a "temporary" definition used in the construction of complex numbers, and is intended to be used only by the construction.) (Contributed by Jim Kingdon, 25-Sep-2019.)

Assertion

Ref	Expression
df-inp	⊢ P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))))}

Distinct variable group:   𝑢,𝑙,𝑞,𝑟

Detailed syntax breakdown of Definition df-inp

Step	Hyp	Ref	Expression
1		cnp 7253	. 2 class P
2		vl	. . . . . . . 8 setvar 𝑙
3	2	cv 1347	. . . . . . 7 class 𝑙
4		cnq 7242	. . . . . . 7 class Q
5	3, 4	wss 3121	. . . . . 6 wff 𝑙 ⊆ Q
6		vu	. . . . . . . 8 setvar 𝑢
7	6	cv 1347	. . . . . . 7 class 𝑢
8	7, 4	wss 3121	. . . . . 6 wff 𝑢 ⊆ Q
9	5, 8	wa 103	. . . . 5 wff (𝑙 ⊆ Q ∧ 𝑢 ⊆ Q)
10		vq	. . . . . . . 8 setvar 𝑞
11	10, 2	wel 2142	. . . . . . 7 wff 𝑞 ∈ 𝑙
12	11, 10, 4	wrex 2449	. . . . . 6 wff ∃𝑞 ∈ Q 𝑞 ∈ 𝑙
13		vr	. . . . . . . 8 setvar 𝑟
14	13, 6	wel 2142	. . . . . . 7 wff 𝑟 ∈ 𝑢
15	14, 13, 4	wrex 2449	. . . . . 6 wff ∃𝑟 ∈ Q 𝑟 ∈ 𝑢
16	12, 15	wa 103	. . . . 5 wff (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)
17	9, 16	wa 103	. . . 4 wff ((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢))
18	10	cv 1347	. . . . . . . . . . 11 class 𝑞
19	13	cv 1347	. . . . . . . . . . 11 class 𝑟
20		cltq 7247	. . . . . . . . . . 11 class <Q
21	18, 19, 20	wbr 3989	. . . . . . . . . 10 wff 𝑞 <Q 𝑟
22	13, 2	wel 2142	. . . . . . . . . 10 wff 𝑟 ∈ 𝑙
23	21, 22	wa 103	. . . . . . . . 9 wff (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)
24	23, 13, 4	wrex 2449	. . . . . . . 8 wff ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)
25	11, 24	wb 104	. . . . . . 7 wff (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙))
26	25, 10, 4	wral 2448	. . . . . 6 wff ∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙))
27	10, 6	wel 2142	. . . . . . . . . 10 wff 𝑞 ∈ 𝑢
28	21, 27	wa 103	. . . . . . . . 9 wff (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢)
29	28, 10, 4	wrex 2449	. . . . . . . 8 wff ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢)
30	14, 29	wb 104	. . . . . . 7 wff (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))
31	30, 13, 4	wral 2448	. . . . . 6 wff ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))
32	26, 31	wa 103	. . . . 5 wff (∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢)))
33	11, 27	wa 103	. . . . . . 7 wff (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢)
34	33	wn 3	. . . . . 6 wff ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢)
35	34, 10, 4	wral 2448	. . . . 5 wff ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢)
36	11, 14	wo 703	. . . . . . . 8 wff (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢)
37	21, 36	wi 4	. . . . . . 7 wff (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))
38	37, 13, 4	wral 2448	. . . . . 6 wff ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))
39	38, 10, 4	wral 2448	. . . . 5 wff ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))
40	32, 35, 39	w3a 973	. . . 4 wff ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢)))
41	17, 40	wa 103	. . 3 wff (((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))))
42	41, 2, 6	copab 4049	. 2 class {⟨𝑙, 𝑢⟩ ∣ (((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))))}
43	1, 42	wceq 1348	1 wff P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙 ⊆ Q ∧ 𝑢 ⊆ Q) ∧ (∃𝑞 ∈ Q 𝑞 ∈ 𝑙 ∧ ∃𝑟 ∈ Q 𝑟 ∈ 𝑢)) ∧ ((∀𝑞 ∈ Q (𝑞 ∈ 𝑙 ↔ ∃𝑟 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑟 ∈ 𝑙)) ∧ ∀𝑟 ∈ Q (𝑟 ∈ 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 <Q 𝑟 ∧ 𝑞 ∈ 𝑢))) ∧ ∀𝑞 ∈ Q ¬ (𝑞 ∈ 𝑙 ∧ 𝑞 ∈ 𝑢) ∧ ∀𝑞 ∈ Q ∀𝑟 ∈ Q (𝑞 <Q 𝑟 → (𝑞 ∈ 𝑙 ∨ 𝑟 ∈ 𝑢))))}

This definition is referenced by:  npsspw  7433  elinp  7436