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

Definition df-iltp 7390
Description: Define ordering on positive reals. We define  x  <P  y if there is a positive fraction  q 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  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) }
Distinct variable group:    x, y, q

Detailed syntax breakdown of Definition df-iltp
StepHypRef Expression
1 cltp 7215 . 2  class  <P
2 vx . . . . . . 7  setvar  x
32cv 1334 . . . . . 6  class  x
4 cnp 7211 . . . . . 6  class  P.
53, 4wcel 2128 . . . . 5  wff  x  e. 
P.
6 vy . . . . . . 7  setvar  y
76cv 1334 . . . . . 6  class  y
87, 4wcel 2128 . . . . 5  wff  y  e. 
P.
95, 8wa 103 . . . 4  wff  ( x  e.  P.  /\  y  e.  P. )
10 vq . . . . . . . 8  setvar  q
1110cv 1334 . . . . . . 7  class  q
12 c2nd 6087 . . . . . . . 8  class  2nd
133, 12cfv 5170 . . . . . . 7  class  ( 2nd `  x )
1411, 13wcel 2128 . . . . . 6  wff  q  e.  ( 2nd `  x
)
15 c1st 6086 . . . . . . . 8  class  1st
167, 15cfv 5170 . . . . . . 7  class  ( 1st `  y )
1711, 16wcel 2128 . . . . . 6  wff  q  e.  ( 1st `  y
)
1814, 17wa 103 . . . . 5  wff  ( q  e.  ( 2nd `  x
)  /\  q  e.  ( 1st `  y ) )
19 cnq 7200 . . . . 5  class  Q.
2018, 10, 19wrex 2436 . . . 4  wff  E. q  e.  Q.  ( q  e.  ( 2nd `  x
)  /\  q  e.  ( 1st `  y ) )
219, 20wa 103 . . 3  wff  ( ( x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) )
2221, 2, 6copab 4024 . 2  class  { <. x ,  y >.  |  ( ( x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) }
231, 22wceq 1335 1  wff  <P  =  { <. x ,  y
>.  |  ( (
x  e.  P.  /\  y  e.  P. )  /\  E. q  e.  Q.  ( q  e.  ( 2nd `  x )  /\  q  e.  ( 1st `  y ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  ltrelpr  7425  ltdfpr  7426
  Copyright terms: Public domain W3C validator