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

Definition df-iltp 6453
Description: Define ordering on positive reals. We define  <P if there is a positive fraction  q 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  <P  { <. , 
>.  |  P.  P.  q  Q. 
q  2nd `  q  1st `  }
Distinct variable group:   ,, q

Detailed syntax breakdown of Definition df-iltp
StepHypRef Expression
1 cltp 6279 . 2  <P
2 vx . . . . . . 7  setvar
32cv 1241 . . . . . 6
4 cnp 6275 . . . . . 6  P.
53, 4wcel 1390 . . . . 5  P.
6 vy . . . . . . 7  setvar
76cv 1241 . . . . . 6
87, 4wcel 1390 . . . . 5  P.
95, 8wa 97 . . . 4  P.  P.
10 vq . . . . . . . 8  setvar  q
1110cv 1241 . . . . . . 7  q
12 c2nd 5708 . . . . . . . 8  2nd
133, 12cfv 4845 . . . . . . 7  2nd `
1411, 13wcel 1390 . . . . . 6  q  2nd `
15 c1st 5707 . . . . . . . 8  1st
167, 15cfv 4845 . . . . . . 7  1st `
1711, 16wcel 1390 . . . . . 6  q  1st `
1814, 17wa 97 . . . . 5 
q  2nd `  q  1st `
19 cnq 6264 . . . . 5  Q.
2018, 10, 19wrex 2301 . . . 4  q  Q.  q  2nd `  q  1st `
219, 20wa 97 . . 3  P.  P.  q  Q.  q  2nd `  q  1st `
2221, 2, 6copab 3808 . 2  { <. ,  >.  |  P.  P.  q  Q.  q  2nd `  q  1st `  }
231, 22wceq 1242 1  <P  { <. , 
>.  |  P.  P.  q  Q. 
q  2nd `  q  1st `  }
Colors of variables: wff set class
This definition is referenced by:  ltrelpr  6488  ltdfpr  6489
  Copyright terms: Public domain W3C validator