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

Definition df-inp 7464
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 7289 . 2 class P
2 vl . . . . . . . 8 setvar 𝑙
32cv 1352 . . . . . . 7 class 𝑙
4 cnq 7278 . . . . . . 7 class Q
53, 4wss 3129 . . . . . 6 wff 𝑙Q
6 vu . . . . . . . 8 setvar 𝑢
76cv 1352 . . . . . . 7 class 𝑢
87, 4wss 3129 . . . . . 6 wff 𝑢Q
95, 8wa 104 . . . . 5 wff (𝑙Q𝑢Q)
10 vq . . . . . . . 8 setvar 𝑞
1110, 2wel 2149 . . . . . . 7 wff 𝑞𝑙
1211, 10, 4wrex 2456 . . . . . 6 wff 𝑞Q 𝑞𝑙
13 vr . . . . . . . 8 setvar 𝑟
1413, 6wel 2149 . . . . . . 7 wff 𝑟𝑢
1514, 13, 4wrex 2456 . . . . . 6 wff 𝑟Q 𝑟𝑢
1612, 15wa 104 . . . . 5 wff (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)
179, 16wa 104 . . . 4 wff ((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢))
1810cv 1352 . . . . . . . . . . 11 class 𝑞
1913cv 1352 . . . . . . . . . . 11 class 𝑟
20 cltq 7283 . . . . . . . . . . 11 class <Q
2118, 19, 20wbr 4003 . . . . . . . . . 10 wff 𝑞 <Q 𝑟
2213, 2wel 2149 . . . . . . . . . 10 wff 𝑟𝑙
2321, 22wa 104 . . . . . . . . 9 wff (𝑞 <Q 𝑟𝑟𝑙)
2423, 13, 4wrex 2456 . . . . . . . 8 wff 𝑟Q (𝑞 <Q 𝑟𝑟𝑙)
2511, 24wb 105 . . . . . . 7 wff (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙))
2625, 10, 4wral 2455 . . . . . 6 wff 𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙))
2710, 6wel 2149 . . . . . . . . . 10 wff 𝑞𝑢
2821, 27wa 104 . . . . . . . . 9 wff (𝑞 <Q 𝑟𝑞𝑢)
2928, 10, 4wrex 2456 . . . . . . . 8 wff 𝑞Q (𝑞 <Q 𝑟𝑞𝑢)
3014, 29wb 105 . . . . . . 7 wff (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))
3130, 13, 4wral 2455 . . . . . 6 wff 𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))
3226, 31wa 104 . . . . 5 wff (∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢)))
3311, 27wa 104 . . . . . . 7 wff (𝑞𝑙𝑞𝑢)
3433wn 3 . . . . . 6 wff ¬ (𝑞𝑙𝑞𝑢)
3534, 10, 4wral 2455 . . . . 5 wff 𝑞Q ¬ (𝑞𝑙𝑞𝑢)
3611, 14wo 708 . . . . . . . 8 wff (𝑞𝑙𝑟𝑢)
3721, 36wi 4 . . . . . . 7 wff (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))
3837, 13, 4wral 2455 . . . . . 6 wff 𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))
3938, 10, 4wral 2455 . . . . 5 wff 𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))
4032, 35, 39w3a 978 . . . 4 wff ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢)))
4117, 40wa 104 . . 3 wff (((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)) ∧ ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))))
4241, 2, 6copab 4063 . 2 class {⟨𝑙, 𝑢⟩ ∣ (((𝑙Q𝑢Q) ∧ (∃𝑞Q 𝑞𝑙 ∧ ∃𝑟Q 𝑟𝑢)) ∧ ((∀𝑞Q (𝑞𝑙 ↔ ∃𝑟Q (𝑞 <Q 𝑟𝑟𝑙)) ∧ ∀𝑟Q (𝑟𝑢 ↔ ∃𝑞Q (𝑞 <Q 𝑟𝑞𝑢))) ∧ ∀𝑞Q ¬ (𝑞𝑙𝑞𝑢) ∧ ∀𝑞Q𝑟Q (𝑞 <Q 𝑟 → (𝑞𝑙𝑟𝑢))))}
431, 42wceq 1353 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  7469  elinp  7472
  Copyright terms: Public domain W3C validator