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

Definition df-iltp 6445
Description: Define ordering on positive reals. We define x<P y if there is a positive fraction 𝑞 which is an element of the upper cut of x and the lower cut of y. From the definition of < in Section 11.2.1 of [HoTT], p. (varies).

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

Assertion
Ref Expression
df-iltp <P = {⟨x, y⟩ ∣ ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))}
Distinct variable group:   x,y,𝑞

Detailed syntax breakdown of Definition df-iltp
StepHypRef Expression
1 cltp 6272 . 2 class <P
2 vx . . . . . . 7 setvar x
32cv 1241 . . . . . 6 class x
4 cnp 6268 . . . . . 6 class P
53, 4wcel 1390 . . . . 5 wff x P
6 vy . . . . . . 7 setvar y
76cv 1241 . . . . . 6 class y
87, 4wcel 1390 . . . . 5 wff y P
95, 8wa 97 . . . 4 wff (x P y P)
10 vq . . . . . . . 8 setvar 𝑞
1110cv 1241 . . . . . . 7 class 𝑞
12 c2nd 5705 . . . . . . . 8 class 2nd
133, 12cfv 4844 . . . . . . 7 class (2ndx)
1411, 13wcel 1390 . . . . . 6 wff 𝑞 (2ndx)
15 c1st 5704 . . . . . . . 8 class 1st
167, 15cfv 4844 . . . . . . 7 class (1sty)
1711, 16wcel 1390 . . . . . 6 wff 𝑞 (1sty)
1814, 17wa 97 . . . . 5 wff (𝑞 (2ndx) 𝑞 (1sty))
19 cnq 6257 . . . . 5 class Q
2018, 10, 19wrex 2301 . . . 4 wff 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty))
219, 20wa 97 . . 3 wff ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))
2221, 2, 6copab 3807 . 2 class {⟨x, y⟩ ∣ ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))}
231, 22wceq 1242 1 wff <P = {⟨x, y⟩ ∣ ((x P y P) 𝑞 Q (𝑞 (2ndx) 𝑞 (1sty)))}
Colors of variables: wff set class
This definition is referenced by:  ltrelpr  6480  ltdfpr  6481
  Copyright terms: Public domain W3C validator