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

Definition df-inp 6448
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 u which is inhabited (𝑞 Q𝑞 𝑙 𝑟 Q𝑟 u), rounded (𝑞 Q(𝑞 𝑙𝑟 Q(𝑞 <Q 𝑟 𝑟 𝑙)) and likewise for u), disjoint (𝑞 Q¬ (𝑞 𝑙 𝑞 u)) and located (𝑞 Q𝑟 Q(𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))). 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 = {⟨𝑙, u⟩ ∣ (((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))))}
Distinct variable group:   u,𝑙,𝑞,𝑟

Detailed syntax breakdown of Definition df-inp
StepHypRef Expression
1 cnp 6275 . 2 class P
2 vl . . . . . . . 8 setvar 𝑙
32cv 1241 . . . . . . 7 class 𝑙
4 cnq 6264 . . . . . . 7 class Q
53, 4wss 2911 . . . . . 6 wff 𝑙Q
6 vu . . . . . . . 8 setvar u
76cv 1241 . . . . . . 7 class u
87, 4wss 2911 . . . . . 6 wff uQ
95, 8wa 97 . . . . 5 wff (𝑙Q uQ)
10 vq . . . . . . . 8 setvar 𝑞
1110, 2wel 1391 . . . . . . 7 wff 𝑞 𝑙
1211, 10, 4wrex 2301 . . . . . 6 wff 𝑞 Q 𝑞 𝑙
13 vr . . . . . . . 8 setvar 𝑟
1413, 6wel 1391 . . . . . . 7 wff 𝑟 u
1514, 13, 4wrex 2301 . . . . . 6 wff 𝑟 Q 𝑟 u
1612, 15wa 97 . . . . 5 wff (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)
179, 16wa 97 . . . 4 wff ((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u))
1810cv 1241 . . . . . . . . . . 11 class 𝑞
1913cv 1241 . . . . . . . . . . 11 class 𝑟
20 cltq 6269 . . . . . . . . . . 11 class <Q
2118, 19, 20wbr 3755 . . . . . . . . . 10 wff 𝑞 <Q 𝑟
2213, 2wel 1391 . . . . . . . . . 10 wff 𝑟 𝑙
2321, 22wa 97 . . . . . . . . 9 wff (𝑞 <Q 𝑟 𝑟 𝑙)
2423, 13, 4wrex 2301 . . . . . . . 8 wff 𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)
2511, 24wb 98 . . . . . . 7 wff (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙))
2625, 10, 4wral 2300 . . . . . 6 wff 𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙))
2710, 6wel 1391 . . . . . . . . . 10 wff 𝑞 u
2821, 27wa 97 . . . . . . . . 9 wff (𝑞 <Q 𝑟 𝑞 u)
2928, 10, 4wrex 2301 . . . . . . . 8 wff 𝑞 Q (𝑞 <Q 𝑟 𝑞 u)
3014, 29wb 98 . . . . . . 7 wff (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))
3130, 13, 4wral 2300 . . . . . 6 wff 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))
3226, 31wa 97 . . . . 5 wff (𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u)))
3311, 27wa 97 . . . . . . 7 wff (𝑞 𝑙 𝑞 u)
3433wn 3 . . . . . 6 wff ¬ (𝑞 𝑙 𝑞 u)
3534, 10, 4wral 2300 . . . . 5 wff 𝑞 Q ¬ (𝑞 𝑙 𝑞 u)
3611, 14wo 628 . . . . . . . 8 wff (𝑞 𝑙 𝑟 u)
3721, 36wi 4 . . . . . . 7 wff (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))
3837, 13, 4wral 2300 . . . . . 6 wff 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))
3938, 10, 4wral 2300 . . . . 5 wff 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))
4032, 35, 39w3a 884 . . . 4 wff ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u)))
4117, 40wa 97 . . 3 wff (((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))))
4241, 2, 6copab 3808 . 2 class {⟨𝑙, u⟩ ∣ (((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))))}
431, 42wceq 1242 1 wff P = {⟨𝑙, u⟩ ∣ (((𝑙Q uQ) (𝑞 Q 𝑞 𝑙 𝑟 Q 𝑟 u)) ((𝑞 Q (𝑞 𝑙𝑟 Q (𝑞 <Q 𝑟 𝑟 𝑙)) 𝑟 Q (𝑟 u𝑞 Q (𝑞 <Q 𝑟 𝑞 u))) 𝑞 Q ¬ (𝑞 𝑙 𝑞 u) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝑙 𝑟 u))))}
Colors of variables: wff set class
This definition is referenced by:  npsspw  6453  elinp  6456
  Copyright terms: Public domain W3C validator