ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-inp GIF version

Definition df-inp 7242
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
StepHypRef Expression
1 cnp 7067 . 2 class P
2 vl . . . . . . . 8 setvar 𝑙
32cv 1315 . . . . . . 7 class 𝑙
4 cnq 7056 . . . . . . 7 class Q
53, 4wss 3041 . . . . . 6 wff 𝑙Q
6 vu . . . . . . . 8 setvar 𝑢
76cv 1315 . . . . . . 7 class 𝑢
87, 4wss 3041 . . . . . 6 wff 𝑢Q
95, 8wa 103 . . . . 5 wff (𝑙Q𝑢Q)
10 vq . . . . . . . 8 setvar 𝑞
1110, 2wel 1466 . . . . . . 7 wff 𝑞𝑙
1211, 10, 4wrex 2394 . . . . . 6 wff 𝑞Q 𝑞𝑙
13 vr . . . . . . . 8 setvar 𝑟
1413, 6wel 1466 . . . . . . 7 wff 𝑟𝑢
1514, 13, 4wrex 2394 . . . . . 6 wff 𝑟Q 𝑟𝑢
1612, 15wa 103 . . . . 5 wff (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)
179, 16wa 103 . . . 4 wff ((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢))
1810cv 1315 . . . . . . . . . . 11 class 𝑞
1913cv 1315 . . . . . . . . . . 11 class 𝑟
20 cltq 7061 . . . . . . . . . . 11 class <Q
2118, 19, 20wbr 3899 . . . . . . . . . 10 wff 𝑞 <Q 𝑟
2213, 2wel 1466 . . . . . . . . . 10 wff 𝑟𝑙
2321, 22wa 103 . . . . . . . . 9 wff (𝑞 <Q 𝑟𝑟𝑙)
2423, 13, 4wrex 2394 . . . . . . . 8 wff 𝑟Q (𝑞 <Q 𝑟𝑟𝑙)
2511, 24wb 104 . . . . . . 7 wff (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙))
2625, 10, 4wral 2393 . . . . . 6 wff 𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙))
2710, 6wel 1466 . . . . . . . . . 10 wff 𝑞𝑢
2821, 27wa 103 . . . . . . . . 9 wff (𝑞 <Q 𝑟𝑞𝑢)
2928, 10, 4wrex 2394 . . . . . . . 8 wff 𝑞Q (𝑞 <Q 𝑟𝑞𝑢)
3014, 29wb 104 . . . . . . 7 wff (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))
3130, 13, 4wral 2393 . . . . . 6 wff 𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))
3226, 31wa 103 . . . . 5 wff (∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢)))
3311, 27wa 103 . . . . . . 7 wff (𝑞𝑙𝑞𝑢)
3433wn 3 . . . . . 6 wff ¬ (𝑞𝑙𝑞𝑢)
3534, 10, 4wral 2393 . . . . 5 wff 𝑞Q ¬ (𝑞𝑙𝑞𝑢)
3611, 14wo 682 . . . . . . . 8 wff (𝑞𝑙𝑟𝑢)
3721, 36wi 4 . . . . . . 7 wff (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))
3837, 13, 4wral 2393 . . . . . 6 wff 𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))
3938, 10, 4wral 2393 . . . . 5 wff 𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))
4032, 35, 39w3a 947 . . . 4 wff ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢)))
4117, 40wa 103 . . 3 wff (((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)) ∧ ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))))
4241, 2, 6copab 3958 . 2 class {⟨𝑙, 𝑢⟩ ∣ (((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)) ∧ ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))))}
431, 42wceq 1316 1 wff P = {⟨𝑙, 𝑢⟩ ∣ (((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)) ∧ ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))))}
Colors of variables: wff set class
This definition is referenced by:  npsspw  7247  elinp  7250
  Copyright terms: Public domain W3C validator