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

Definition df-inp 6564
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 6389 . 2  class  P.
2 vl . . . . . . . 8  setvar  l
32cv 1242 . . . . . . 7  class  l
4 cnq 6378 . . . . . . 7  class  Q.
53, 4wss 2917 . . . . . 6  wff  l  C_  Q.
6 vu . . . . . . . 8  setvar  u
76cv 1242 . . . . . . 7  class  u
87, 4wss 2917 . . . . . 6  wff  u  C_  Q.
95, 8wa 97 . . . . 5  wff  ( l 
C_  Q.  /\  u  C_ 
Q. )
10 vq . . . . . . . 8  setvar  q
1110, 2wel 1394 . . . . . . 7  wff  q  e.  l
1211, 10, 4wrex 2307 . . . . . 6  wff  E. q  e.  Q.  q  e.  l
13 vr . . . . . . . 8  setvar  r
1413, 6wel 1394 . . . . . . 7  wff  r  e.  u
1514, 13, 4wrex 2307 . . . . . 6  wff  E. r  e.  Q.  r  e.  u
1612, 15wa 97 . . . . 5  wff  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u
)
179, 16wa 97 . . . 4  wff  ( ( l  C_  Q.  /\  u  C_ 
Q. )  /\  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u ) )
1810cv 1242 . . . . . . . . . . 11  class  q
1913cv 1242 . . . . . . . . . . 11  class  r
20 cltq 6383 . . . . . . . . . . 11  class  <Q
2118, 19, 20wbr 3764 . . . . . . . . . 10  wff  q  <Q 
r
2213, 2wel 1394 . . . . . . . . . 10  wff  r  e.  l
2321, 22wa 97 . . . . . . . . 9  wff  ( q 
<Q  r  /\  r  e.  l )
2423, 13, 4wrex 2307 . . . . . . . 8  wff  E. r  e.  Q.  ( q  <Q 
r  /\  r  e.  l )
2511, 24wb 98 . . . . . . 7  wff  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q 
r  /\  r  e.  l ) )
2625, 10, 4wral 2306 . . . . . 6  wff  A. q  e.  Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )
2710, 6wel 1394 . . . . . . . . . 10  wff  q  e.  u
2821, 27wa 97 . . . . . . . . 9  wff  ( q 
<Q  r  /\  q  e.  u )
2928, 10, 4wrex 2307 . . . . . . . 8  wff  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u )
3014, 29wb 98 . . . . . . 7  wff  ( r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) )
3130, 13, 4wral 2306 . . . . . 6  wff  A. r  e.  Q.  ( r  e.  u  <->  E. q  e.  Q.  ( q  <Q  r  /\  q  e.  u
) )
3226, 31wa 97 . . . . 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 97 . . . . . . 7  wff  ( q  e.  l  /\  q  e.  u )
3433wn 3 . . . . . 6  wff  -.  (
q  e.  l  /\  q  e.  u )
3534, 10, 4wral 2306 . . . . 5  wff  A. q  e.  Q.  -.  ( q  e.  l  /\  q  e.  u )
3611, 14wo 629 . . . . . . . 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 2306 . . . . . 6  wff  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) )
3938, 10, 4wral 2306 . . . . 5  wff  A. q  e.  Q.  A. r  e. 
Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) )
4032, 35, 39w3a 885 . . . 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 97 . . 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 3817 . 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 1243 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  6569  elinp  6572
  Copyright terms: Public domain W3C validator