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

Definition df-inp 6621
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 6446 . 2  class  P.
2 vl . . . . . . . 8  setvar  l
32cv 1258 . . . . . . 7  class  l
4 cnq 6435 . . . . . . 7  class  Q.
53, 4wss 2944 . . . . . 6  wff  l  C_  Q.
6 vu . . . . . . . 8  setvar  u
76cv 1258 . . . . . . 7  class  u
87, 4wss 2944 . . . . . 6  wff  u  C_  Q.
95, 8wa 101 . . . . 5  wff  ( l 
C_  Q.  /\  u  C_ 
Q. )
10 vq . . . . . . . 8  setvar  q
1110, 2wel 1410 . . . . . . 7  wff  q  e.  l
1211, 10, 4wrex 2324 . . . . . 6  wff  E. q  e.  Q.  q  e.  l
13 vr . . . . . . . 8  setvar  r
1413, 6wel 1410 . . . . . . 7  wff  r  e.  u
1514, 13, 4wrex 2324 . . . . . 6  wff  E. r  e.  Q.  r  e.  u
1612, 15wa 101 . . . . 5  wff  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u
)
179, 16wa 101 . . . 4  wff  ( ( l  C_  Q.  /\  u  C_ 
Q. )  /\  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u ) )
1810cv 1258 . . . . . . . . . . 11  class  q
1913cv 1258 . . . . . . . . . . 11  class  r
20 cltq 6440 . . . . . . . . . . 11  class  <Q
2118, 19, 20wbr 3791 . . . . . . . . . 10  wff  q  <Q 
r
2213, 2wel 1410 . . . . . . . . . 10  wff  r  e.  l
2321, 22wa 101 . . . . . . . . 9  wff  ( q 
<Q  r  /\  r  e.  l )
2423, 13, 4wrex 2324 . . . . . . . 8  wff  E. r  e.  Q.  ( q  <Q 
r  /\  r  e.  l )
2511, 24wb 102 . . . . . . 7  wff  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q 
r  /\  r  e.  l ) )
2625, 10, 4wral 2323 . . . . . 6  wff  A. q  e.  Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )
2710, 6wel 1410 . . . . . . . . . 10  wff  q  e.  u
2821, 27wa 101 . . . . . . . . 9  wff  ( q 
<Q  r  /\  q  e.  u )
2928, 10, 4wrex 2324 . . . . . . . 8  wff  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u )
3014, 29wb 102 . . . . . . 7  wff  ( r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) )
3130, 13, 4wral 2323 . . . . . 6  wff  A. r  e.  Q.  ( r  e.  u  <->  E. q  e.  Q.  ( q  <Q  r  /\  q  e.  u
) )
3226, 31wa 101 . . . . 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 101 . . . . . . 7  wff  ( q  e.  l  /\  q  e.  u )
3433wn 3 . . . . . 6  wff  -.  (
q  e.  l  /\  q  e.  u )
3534, 10, 4wral 2323 . . . . 5  wff  A. q  e.  Q.  -.  ( q  e.  l  /\  q  e.  u )
3611, 14wo 639 . . . . . . . 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 2323 . . . . . 6  wff  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) )
3938, 10, 4wral 2323 . . . . 5  wff  A. q  e.  Q.  A. r  e. 
Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) )
4032, 35, 39w3a 896 . . . 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 101 . . 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 3844 . 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 1259 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  6626  elinp  6629
  Copyright terms: Public domain W3C validator