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

Definition df-ltr 6658
Description: Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.)
Assertion
Ref Expression
df-ltr  <R  { <. , 
>.  |  R.  R.  <. ,  >.  ~R  <. ,  >.  ~R  +P.  <P  +P.  }
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-ltr
StepHypRef Expression
1 cltr 6287 . 2  <R
2 vx . . . . . . 7  setvar
32cv 1241 . . . . . 6
4 cnr 6281 . . . . . 6  R.
53, 4wcel 1390 . . . . 5  R.
6 vy . . . . . . 7  setvar
76cv 1241 . . . . . 6
87, 4wcel 1390 . . . . 5  R.
95, 8wa 97 . . . 4  R.  R.
10 vz . . . . . . . . . . . . . 14  setvar
1110cv 1241 . . . . . . . . . . . . 13
12 vw . . . . . . . . . . . . . 14  setvar
1312cv 1241 . . . . . . . . . . . . 13
1411, 13cop 3370 . . . . . . . . . . . 12  <. ,  >.
15 cer 6280 . . . . . . . . . . . 12  ~R
1614, 15cec 6040 . . . . . . . . . . 11  <. ,  >.  ~R
173, 16wceq 1242 . . . . . . . . . 10  <. ,  >.  ~R
18 vv . . . . . . . . . . . . . 14  setvar
1918cv 1241 . . . . . . . . . . . . 13
20 vu . . . . . . . . . . . . . 14  setvar
2120cv 1241 . . . . . . . . . . . . 13
2219, 21cop 3370 . . . . . . . . . . . 12  <. ,  >.
2322, 15cec 6040 . . . . . . . . . . 11  <. ,  >.  ~R
247, 23wceq 1242 . . . . . . . . . 10  <. ,  >.  ~R
2517, 24wa 97 . . . . . . . . 9  <. ,  >.  ~R  <. ,  >.  ~R
26 cpp 6277 . . . . . . . . . . 11  +P.
2711, 21, 26co 5455 . . . . . . . . . 10 
+P.
2813, 19, 26co 5455 . . . . . . . . . 10 
+P.
29 cltp 6279 . . . . . . . . . 10  <P
3027, 28, 29wbr 3755 . . . . . . . . 9  +P.  <P  +P.
3125, 30wa 97 . . . . . . . 8  <. ,  >. 
~R  <. ,  >.  ~R  +P. 
<P  +P.
3231, 20wex 1378 . . . . . . 7  <. ,  >. 
~R  <. ,  >.  ~R  +P. 
<P  +P.
3332, 18wex 1378 . . . . . 6  <. ,  >.  ~R  <. ,  >.  ~R  +P.  <P  +P.
3433, 12wex 1378 . . . . 5  <. ,  >. 
~R  <. ,  >.  ~R  +P. 
<P  +P.
3534, 10wex 1378 . . . 4  <. ,  >.  ~R  <. ,  >.  ~R  +P. 
<P  +P.
369, 35wa 97 . . 3  R.  R.  <. ,  >. 
~R  <. ,  >.  ~R  +P. 
<P  +P.
3736, 2, 6copab 3808 . 2  { <. ,  >.  |  R.  R.  <. ,  >. 
~R  <. ,  >.  ~R  +P. 
<P  +P.  }
381, 37wceq 1242 1  <R  { <. , 
>.  |  R.  R.  <. ,  >.  ~R  <. ,  >.  ~R  +P.  <P  +P.  }
Colors of variables: wff set class
This definition is referenced by:  ltrelsr  6666  ltsrprg  6675
  Copyright terms: Public domain W3C validator