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

Definition df-iltp 7271
 Description: Define ordering on positive reals. We define if there is a positive fraction which is an element of the upper cut of and the lower cut of . 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-iltp
StepHypRef Expression
1 cltp 7096 . 2
2 vx . . . . . . 7
32cv 1330 . . . . . 6
4 cnp 7092 . . . . . 6
53, 4wcel 1480 . . . . 5
6 vy . . . . . . 7
76cv 1330 . . . . . 6
87, 4wcel 1480 . . . . 5
95, 8wa 103 . . . 4
10 vq . . . . . . . 8
1110cv 1330 . . . . . . 7
12 c2nd 6030 . . . . . . . 8
133, 12cfv 5118 . . . . . . 7
1411, 13wcel 1480 . . . . . 6
15 c1st 6029 . . . . . . . 8
167, 15cfv 5118 . . . . . . 7
1711, 16wcel 1480 . . . . . 6
1814, 17wa 103 . . . . 5
19 cnq 7081 . . . . 5
2018, 10, 19wrex 2415 . . . 4
219, 20wa 103 . . 3
2221, 2, 6copab 3983 . 2
231, 22wceq 1331 1
 Colors of variables: wff set class This definition is referenced by:  ltrelpr  7306  ltdfpr  7307
 Copyright terms: Public domain W3C validator