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

Definition df-inp 7286
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 7111 . 2  class  P.
2 vl . . . . . . . 8  setvar  l
32cv 1330 . . . . . . 7  class  l
4 cnq 7100 . . . . . . 7  class  Q.
53, 4wss 3071 . . . . . 6  wff  l  C_  Q.
6 vu . . . . . . . 8  setvar  u
76cv 1330 . . . . . . 7  class  u
87, 4wss 3071 . . . . . 6  wff  u  C_  Q.
95, 8wa 103 . . . . 5  wff  ( l 
C_  Q.  /\  u  C_ 
Q. )
10 vq . . . . . . . 8  setvar  q
1110, 2wel 1481 . . . . . . 7  wff  q  e.  l
1211, 10, 4wrex 2417 . . . . . 6  wff  E. q  e.  Q.  q  e.  l
13 vr . . . . . . . 8  setvar  r
1413, 6wel 1481 . . . . . . 7  wff  r  e.  u
1514, 13, 4wrex 2417 . . . . . 6  wff  E. r  e.  Q.  r  e.  u
1612, 15wa 103 . . . . 5  wff  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u
)
179, 16wa 103 . . . 4  wff  ( ( l  C_  Q.  /\  u  C_ 
Q. )  /\  ( E. q  e.  Q.  q  e.  l  /\  E. r  e.  Q.  r  e.  u ) )
1810cv 1330 . . . . . . . . . . 11  class  q
1913cv 1330 . . . . . . . . . . 11  class  r
20 cltq 7105 . . . . . . . . . . 11  class  <Q
2118, 19, 20wbr 3929 . . . . . . . . . 10  wff  q  <Q 
r
2213, 2wel 1481 . . . . . . . . . 10  wff  r  e.  l
2321, 22wa 103 . . . . . . . . 9  wff  ( q 
<Q  r  /\  r  e.  l )
2423, 13, 4wrex 2417 . . . . . . . 8  wff  E. r  e.  Q.  ( q  <Q 
r  /\  r  e.  l )
2511, 24wb 104 . . . . . . 7  wff  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q 
r  /\  r  e.  l ) )
2625, 10, 4wral 2416 . . . . . 6  wff  A. q  e.  Q.  ( q  e.  l  <->  E. r  e.  Q.  ( q  <Q  r  /\  r  e.  l
) )
2710, 6wel 1481 . . . . . . . . . 10  wff  q  e.  u
2821, 27wa 103 . . . . . . . . 9  wff  ( q 
<Q  r  /\  q  e.  u )
2928, 10, 4wrex 2417 . . . . . . . 8  wff  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u )
3014, 29wb 104 . . . . . . 7  wff  ( r  e.  u  <->  E. q  e.  Q.  ( q  <Q 
r  /\  q  e.  u ) )
3130, 13, 4wral 2416 . . . . . 6  wff  A. r  e.  Q.  ( r  e.  u  <->  E. q  e.  Q.  ( q  <Q  r  /\  q  e.  u
) )
3226, 31wa 103 . . . . 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 103 . . . . . . 7  wff  ( q  e.  l  /\  q  e.  u )
3433wn 3 . . . . . 6  wff  -.  (
q  e.  l  /\  q  e.  u )
3534, 10, 4wral 2416 . . . . 5  wff  A. q  e.  Q.  -.  ( q  e.  l  /\  q  e.  u )
3611, 14wo 697 . . . . . . . 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 2416 . . . . . 6  wff  A. r  e.  Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) )
3938, 10, 4wral 2416 . . . . 5  wff  A. q  e.  Q.  A. r  e. 
Q.  ( q  <Q 
r  ->  ( q  e.  l  \/  r  e.  u ) )
4032, 35, 39w3a 962 . . . 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 103 . . 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 3988 . 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 1331 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  7291  elinp  7294
  Copyright terms: Public domain W3C validator