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

Definition df-inp 6969
Description: Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other.

Here we follow the definition of a Dedekind cut from Definition 11.2.1 of [HoTT], p. (varies) with the one exception that we define it over positive rational numbers rather than all rational numbers.

A Dedekind cut is an ordered pair of a lower set  l and an upper set  u which is inhabited ( E. q  e. 
Q. q  e.  l  /\  E. r  e. 
Q. r  e.  u), rounded ( A. q  e.  Q. ( q  e.  l  <->  E. r  e.  Q. ( q  <Q  r  /\  r  e.  l
) ) and likewise for  u), disjoint ( A. q  e. 
Q. -.  ( q  e.  l  /\  q  e.  u )) and located ( A. q  e. 
Q. A. r  e.  Q. ( q  <Q  r  ->  ( q  e.  l  \/  r  e.  u
) )). See HoTT for more discussion of those terms and different ways of defining Dedekind cuts.

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

Assertion
Ref Expression
df-inp  |-  P.  =  { <. l ,  u >.  |  ( ( ( l  C_  Q.  /\  u  C_ 
Q. )  /\  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u ) )  /\  ( ( A. q  e.  Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )  /\  A. r  e.  Q.  (
r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) ) )  /\  A. q  e. 
Q.  -.  ( q  e.  l  /\  q  e.  u )  /\  A. q  e.  Q.  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) ) ) ) }
Distinct variable group:    u, l, q, r

Detailed syntax breakdown of Definition df-inp
StepHypRef Expression
1 cnp 6794 . 2  class  P.
2 vl . . . . . . . 8  setvar  l
32cv 1286 . . . . . . 7  class  l
4 cnq 6783 . . . . . . 7  class  Q.
53, 4wss 2988 . . . . . 6  wff  l  C_  Q.
6 vu . . . . . . . 8  setvar  u
76cv 1286 . . . . . . 7  class  u
87, 4wss 2988 . . . . . 6  wff  u  C_  Q.
95, 8wa 102 . . . . 5  wff  ( l 
C_  Q.  /\  u  C_ 
Q. )
10 vq . . . . . . . 8  setvar  q
1110, 2wel 1437 . . . . . . 7  wff  q  e.  l
1211, 10, 4wrex 2356 . . . . . 6  wff  E. q  e.  Q.  q  e.  l
13 vr . . . . . . . 8  setvar  r
1413, 6wel 1437 . . . . . . 7  wff  r  e.  u
1514, 13, 4wrex 2356 . . . . . 6  wff  E. r  e.  Q.  r  e.  u
1612, 15wa 102 . . . . 5  wff  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u
)
179, 16wa 102 . . . 4  wff  ( ( l  C_  Q.  /\  u  C_ 
Q. )  /\  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u ) )
1810cv 1286 . . . . . . . . . . 11  class  q
1913cv 1286 . . . . . . . . . . 11  class  r
20 cltq 6788 . . . . . . . . . . 11  class  <Q
2118, 19, 20wbr 3820 . . . . . . . . . 10  wff  q  <Q 
r
2213, 2wel 1437 . . . . . . . . . 10  wff  r  e.  l
2321, 22wa 102 . . . . . . . . 9  wff  ( q 
<Q  r  /\  r  e.  l )
2423, 13, 4wrex 2356 . . . . . . . 8  wff  E. r  e.  Q.  ( q  <Q 
r  /\  r  e.  l )
2511, 24wb 103 . . . . . . 7  wff  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q 
r  /\  r  e.  l ) )
2625, 10, 4wral 2355 . . . . . 6  wff  A. q  e.  Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )
2710, 6wel 1437 . . . . . . . . . 10  wff  q  e.  u
2821, 27wa 102 . . . . . . . . 9  wff  ( q 
<Q  r  /\  q  e.  u )
2928, 10, 4wrex 2356 . . . . . . . 8  wff  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u )
3014, 29wb 103 . . . . . . 7  wff  ( r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) )
3130, 13, 4wral 2355 . . . . . 6  wff  A. r  e.  Q.  ( r  e.  u  <->  E. q  e.  Q.  ( q  <Q  r  /\  q  e.  u
) )
3226, 31wa 102 . . . . 5  wff  ( A. q  e.  Q.  (
q  e.  l  <->  E. r  e.  Q.  ( q  <Q 
r  /\  r  e.  l ) )  /\  A. r  e.  Q.  (
r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) ) )
3311, 27wa 102 . . . . . . 7  wff  ( q  e.  l  /\  q  e.  u )
3433wn 3 . . . . . 6  wff  -.  (
q  e.  l  /\  q  e.  u )
3534, 10, 4wral 2355 . . . . 5  wff  A. q  e.  Q.  -.  ( q  e.  l  /\  q  e.  u )
3611, 14wo 662 . . . . . . . 8  wff  ( q  e.  l  \/  r  e.  u )
3721, 36wi 4 . . . . . . 7  wff  ( q 
<Q  r  ->  ( q  e.  l  \/  r  e.  u ) )
3837, 13, 4wral 2355 . . . . . 6  wff  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) )
3938, 10, 4wral 2355 . . . . 5  wff  A. q  e.  Q.  A. r  e. 
Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) )
4032, 35, 39w3a 922 . . . 4  wff  ( ( A. q  e.  Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )  /\  A. r  e.  Q.  (
r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) ) )  /\  A. q  e. 
Q.  -.  ( q  e.  l  /\  q  e.  u )  /\  A. q  e.  Q.  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) ) )
4117, 40wa 102 . . 3  wff  ( ( ( l  C_  Q.  /\  u  C_  Q. )  /\  ( E. q  e. 
Q.  q  e.  l  /\  E. r  e. 
Q.  r  e.  u
) )  /\  (
( A. q  e. 
Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )  /\  A. r  e.  Q.  (
r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) ) )  /\  A. q  e. 
Q.  -.  ( q  e.  l  /\  q  e.  u )  /\  A. q  e.  Q.  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) ) ) )
4241, 2, 6copab 3873 . 2  class  { <. l ,  u >.  |  ( ( ( l  C_  Q.  /\  u  C_  Q. )  /\  ( E. q  e.  Q.  q  e.  l  /\  E. r  e. 
Q.  r  e.  u
) )  /\  (
( A. q  e. 
Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )  /\  A. r  e.  Q.  (
r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) ) )  /\  A. q  e. 
Q.  -.  ( q  e.  l  /\  q  e.  u )  /\  A. q  e.  Q.  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) ) ) ) }
431, 42wceq 1287 1  wff  P.  =  { <. l ,  u >.  |  ( ( ( l  C_  Q.  /\  u  C_ 
Q. )  /\  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u ) )  /\  ( ( A. q  e.  Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )  /\  A. r  e.  Q.  (
r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) ) )  /\  A. q  e. 
Q.  -.  ( q  e.  l  /\  q  e.  u )  /\  A. q  e.  Q.  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  npsspw  6974  elinp  6977
  Copyright terms: Public domain W3C validator