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

Theorem sup3exmid 8976
Description: If any inhabited set of real numbers bounded from above has a supremum, excluded middle follows. (Contributed by Jim Kingdon, 2-Apr-2023.)
Hypothesis
Ref Expression
sup3exmid.ex  |-  ( ( u  C_  RR  /\  E. w  w  e.  u  /\  E. x  e.  RR  A. y  e.  u  y  <_  x )  ->  E. x  e.  RR  ( A. y  e.  u  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  u  y  <  z ) ) )
Assertion
Ref Expression
sup3exmid  |- DECID  ph
Distinct variable groups:    x, z    ph, u, w    ph, x, y, z, u

Proof of Theorem sup3exmid
Dummy variables  a  b  j  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0lt1 8146 . . . 4  |-  0  <  1
2 0re 8019 . . . . 5  |-  0  e.  RR
3 1re 8018 . . . . 5  |-  1  e.  RR
4 lttri3 8099 . . . . . . . 8  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( a  =  b  <-> 
( -.  a  < 
b  /\  -.  b  <  a ) ) )
54adantl 277 . . . . . . 7  |-  ( ( T.  /\  ( a  e.  RR  /\  b  e.  RR ) )  -> 
( a  =  b  <-> 
( -.  a  < 
b  /\  -.  b  <  a ) ) )
6 elrabi 2913 . . . . . . . . . . . 12  |-  ( k  e.  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  k  e. 
{ 0 ,  1 } )
7 elpri 3641 . . . . . . . . . . . 12  |-  ( k  e.  { 0 ,  1 }  ->  (
k  =  0  \/  k  =  1 ) )
86, 7syl 14 . . . . . . . . . . 11  |-  ( k  e.  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( k  =  0  \/  k  =  1 ) )
9 eleq1 2256 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
k  e.  RR  <->  0  e.  RR ) )
102, 9mpbiri 168 . . . . . . . . . . . 12  |-  ( k  =  0  ->  k  e.  RR )
11 eleq1 2256 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
k  e.  RR  <->  1  e.  RR ) )
123, 11mpbiri 168 . . . . . . . . . . . 12  |-  ( k  =  1  ->  k  e.  RR )
1310, 12jaoi 717 . . . . . . . . . . 11  |-  ( ( k  =  0  \/  k  =  1 )  ->  k  e.  RR )
148, 13syl 14 . . . . . . . . . 10  |-  ( k  e.  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  k  e.  RR )
1514ssriv 3183 . . . . . . . . 9  |-  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) }  C_  RR
16 eqid 2193 . . . . . . . . . . . 12  |-  0  =  0
1716orci 732 . . . . . . . . . . 11  |-  ( 0  =  0  \/  ph )
182elexi 2772 . . . . . . . . . . . . 13  |-  0  e.  _V
1918prid1 3724 . . . . . . . . . . . 12  |-  0  e.  { 0 ,  1 }
20 eqeq1 2200 . . . . . . . . . . . . . 14  |-  ( j  =  0  ->  (
j  =  0  <->  0  =  0 ) )
2120orbi1d 792 . . . . . . . . . . . . 13  |-  ( j  =  0  ->  (
( j  =  0  \/  ph )  <->  ( 0  =  0  \/  ph ) ) )
2221elrab3 2917 . . . . . . . . . . . 12  |-  ( 0  e.  { 0 ,  1 }  ->  (
0  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) }  <->  ( 0  =  0  \/  ph ) ) )
2319, 22ax-mp 5 . . . . . . . . . . 11  |-  ( 0  e.  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  <->  ( 0  =  0  \/  ph )
)
2417, 23mpbir 146 . . . . . . . . . 10  |-  0  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }
25 elex2 2776 . . . . . . . . . 10  |-  ( 0  e.  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  E. w  w  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/  ph ) } )
2624, 25ax-mp 5 . . . . . . . . 9  |-  E. w  w  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/  ph ) }
27 elrabi 2913 . . . . . . . . . . . 12  |-  ( y  e.  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  y  e. 
{ 0 ,  1 } )
28 elpri 3641 . . . . . . . . . . . . 13  |-  ( y  e.  { 0 ,  1 }  ->  (
y  =  0  \/  y  =  1 ) )
29 0le1 8500 . . . . . . . . . . . . . . 15  |-  0  <_  1
30 breq1 4032 . . . . . . . . . . . . . . 15  |-  ( y  =  0  ->  (
y  <_  1  <->  0  <_  1 ) )
3129, 30mpbiri 168 . . . . . . . . . . . . . 14  |-  ( y  =  0  ->  y  <_  1 )
323eqlei2 8114 . . . . . . . . . . . . . 14  |-  ( y  =  1  ->  y  <_  1 )
3331, 32jaoi 717 . . . . . . . . . . . . 13  |-  ( ( y  =  0  \/  y  =  1 )  ->  y  <_  1
)
3428, 33syl 14 . . . . . . . . . . . 12  |-  ( y  e.  { 0 ,  1 }  ->  y  <_  1 )
3527, 34syl 14 . . . . . . . . . . 11  |-  ( y  e.  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  y  <_ 
1 )
3635rgen 2547 . . . . . . . . . 10  |-  A. y  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } y  <_  1
37 breq2 4033 . . . . . . . . . . . 12  |-  ( x  =  1  ->  (
y  <_  x  <->  y  <_  1 ) )
3837ralbidv 2494 . . . . . . . . . . 11  |-  ( x  =  1  ->  ( A. y  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } y  <_  x  <->  A. y  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } y  <_  1
) )
3938rspcev 2864 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  A. y  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } y  <_  1 )  ->  E. x  e.  RR  A. y  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } y  <_  x )
403, 36, 39mp2an 426 . . . . . . . . 9  |-  E. x  e.  RR  A. y  e. 
{ j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } y  <_  x
41 prexg 4240 . . . . . . . . . . . 12  |-  ( ( 0  e.  RR  /\  1  e.  RR )  ->  { 0 ,  1 }  e.  _V )
422, 3, 41mp2an 426 . . . . . . . . . . 11  |-  { 0 ,  1 }  e.  _V
4342rabex 4173 . . . . . . . . . 10  |-  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) }  e.  _V
44 sseq1 3202 . . . . . . . . . . . 12  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( u 
C_  RR  <->  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  C_  RR ) )
45 eleq2 2257 . . . . . . . . . . . . 13  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( w  e.  u  <->  w  e.  { j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } ) )
4645exbidv 1836 . . . . . . . . . . . 12  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( E. w  w  e.  u  <->  E. w  w  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } ) )
47 raleq 2690 . . . . . . . . . . . . 13  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( A. y  e.  u  y  <_  x  <->  A. y  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } y  <_  x )
)
4847rexbidv 2495 . . . . . . . . . . . 12  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( E. x  e.  RR  A. y  e.  u  y  <_  x  <->  E. x  e.  RR  A. y  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } y  <_  x ) )
4944, 46, 483anbi123d 1323 . . . . . . . . . . 11  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( ( u  C_  RR  /\  E. w  w  e.  u  /\  E. x  e.  RR  A. y  e.  u  y  <_  x )  <->  ( {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } 
C_  RR  /\  E. w  w  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/  ph ) }  /\  E. x  e.  RR  A. y  e. 
{ j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } y  <_  x
) ) )
50 raleq 2690 . . . . . . . . . . . . 13  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( A. y  e.  u  -.  x  <  y  <->  A. y  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  -.  x  <  y
) )
51 rexeq 2691 . . . . . . . . . . . . . . 15  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( E. z  e.  u  y  <  z  <->  E. z  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } y  <  z
) )
5251imbi2d 230 . . . . . . . . . . . . . 14  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( ( y  <  x  ->  E. z  e.  u  y  <  z )  <->  ( y  <  x  ->  E. z  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } y  <  z
) ) )
5352ralbidv 2494 . . . . . . . . . . . . 13  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( A. y  e.  RR  (
y  <  x  ->  E. z  e.  u  y  <  z )  <->  A. y  e.  RR  ( y  < 
x  ->  E. z  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } y  <  z
) ) )
5450, 53anbi12d 473 . . . . . . . . . . . 12  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( ( A. y  e.  u  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  u  y  <  z ) )  <-> 
( A. y  e. 
{ j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } y  <  z ) ) ) )
5554rexbidv 2495 . . . . . . . . . . 11  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( E. x  e.  RR  ( A. y  e.  u  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  u  y  <  z ) )  <->  E. x  e.  RR  ( A. y  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } y  <  z ) ) ) )
5649, 55imbi12d 234 . . . . . . . . . 10  |-  ( u  =  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  ->  ( ( ( u  C_  RR  /\ 
E. w  w  e.  u  /\  E. x  e.  RR  A. y  e.  u  y  <_  x
)  ->  E. x  e.  RR  ( A. y  e.  u  -.  x  <  y  /\  A. y  e.  RR  ( y  < 
x  ->  E. z  e.  u  y  <  z ) ) )  <->  ( ( { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  C_  RR  /\  E. w  w  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) }  /\  E. x  e.  RR  A. y  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/  ph ) } y  <_  x
)  ->  E. x  e.  RR  ( A. y  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } y  <  z ) ) ) ) )
57 sup3exmid.ex . . . . . . . . . 10  |-  ( ( u  C_  RR  /\  E. w  w  e.  u  /\  E. x  e.  RR  A. y  e.  u  y  <_  x )  ->  E. x  e.  RR  ( A. y  e.  u  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  u  y  <  z ) ) )
5843, 56, 57vtocl 2814 . . . . . . . . 9  |-  ( ( { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  C_  RR  /\  E. w  w  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) }  /\  E. x  e.  RR  A. y  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/  ph ) } y  <_  x
)  ->  E. x  e.  RR  ( A. y  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } y  <  z ) ) )
5915, 26, 40, 58mp3an 1348 . . . . . . . 8  |-  E. x  e.  RR  ( A. y  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } y  <  z ) )
6059a1i 9 . . . . . . 7  |-  ( T. 
->  E. x  e.  RR  ( A. y  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) }  -.  x  <  y  /\  A. y  e.  RR  ( y  <  x  ->  E. z  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } y  <  z ) ) )
615, 60supclti 7057 . . . . . 6  |-  ( T. 
->  sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  e.  RR )
6261mptru 1373 . . . . 5  |-  sup ( { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } ,  RR ,  <  )  e.  RR
63 axltwlin 8087 . . . . 5  |-  ( ( 0  e.  RR  /\  1  e.  RR  /\  sup ( { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } ,  RR ,  <  )  e.  RR )  ->  ( 0  <  1  ->  ( 0  <  sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  \/ 
sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  <  1 ) ) )
642, 3, 62, 63mp3an 1348 . . . 4  |-  ( 0  <  1  ->  (
0  <  sup ( { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } ,  RR ,  <  )  \/  sup ( { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } ,  RR ,  <  )  <  1 ) )
651, 64ax-mp 5 . . 3  |-  ( 0  <  sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  \/ 
sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  <  1 )
665, 60suplubti 7059 . . . . . . . 8  |-  ( T. 
->  ( ( 0  e.  RR  /\  0  <  sup ( { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) } ,  RR ,  <  ) )  ->  E. z  e.  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } 0  <  z
) )
6766mptru 1373 . . . . . . 7  |-  ( ( 0  e.  RR  /\  0  <  sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  ) )  ->  E. z  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } 0  <  z )
682, 67mpan 424 . . . . . 6  |-  ( 0  <  sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  ->  E. z  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } 0  <  z )
69 df-rex 2478 . . . . . 6  |-  ( E. z  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } 0  <  z  <->  E. z
( z  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) }  /\  0  <  z
) )
7068, 69sylib 122 . . . . 5  |-  ( 0  <  sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  ->  E. z ( z  e. 
{ j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  /\  0  <  z
) )
71 eqeq1 2200 . . . . . . . . 9  |-  ( j  =  z  ->  (
j  =  0  <->  z  =  0 ) )
7271orbi1d 792 . . . . . . . 8  |-  ( j  =  z  ->  (
( j  =  0  \/  ph )  <->  ( z  =  0  \/  ph ) ) )
7372elrab 2916 . . . . . . 7  |-  ( z  e.  { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) }  <->  ( z  e. 
{ 0 ,  1 }  /\  ( z  =  0  \/  ph ) ) )
74 simpr 110 . . . . . . . . . 10  |-  ( ( ( z  e.  {
0 ,  1 }  /\  ( z  =  0  \/  ph )
)  /\  0  <  z )  ->  0  <  z )
7574gt0ne0d 8531 . . . . . . . . 9  |-  ( ( ( z  e.  {
0 ,  1 }  /\  ( z  =  0  \/  ph )
)  /\  0  <  z )  ->  z  =/=  0 )
7675neneqd 2385 . . . . . . . 8  |-  ( ( ( z  e.  {
0 ,  1 }  /\  ( z  =  0  \/  ph )
)  /\  0  <  z )  ->  -.  z  =  0 )
77 simplr 528 . . . . . . . 8  |-  ( ( ( z  e.  {
0 ,  1 }  /\  ( z  =  0  \/  ph )
)  /\  0  <  z )  ->  ( z  =  0  \/  ph ) )
78 orel1 726 . . . . . . . 8  |-  ( -.  z  =  0  -> 
( ( z  =  0  \/  ph )  ->  ph ) )
7976, 77, 78sylc 62 . . . . . . 7  |-  ( ( ( z  e.  {
0 ,  1 }  /\  ( z  =  0  \/  ph )
)  /\  0  <  z )  ->  ph )
8073, 79sylanb 284 . . . . . 6  |-  ( ( z  e.  { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) }  /\  0  <  z )  ->  ph )
8180exlimiv 1609 . . . . 5  |-  ( E. z ( z  e. 
{ j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  /\  0  <  z
)  ->  ph )
8270, 81syl 14 . . . 4  |-  ( 0  <  sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  ->  ph )
833ltnri 8112 . . . . . 6  |-  -.  1  <  1
84 iba 300 . . . . . . . . . . . 12  |-  ( ( z  =  0  \/ 
ph )  ->  (
z  e.  { 0 ,  1 }  <->  ( z  e.  { 0 ,  1 }  /\  ( z  =  0  \/  ph ) ) ) )
8584olcs 737 . . . . . . . . . . 11  |-  ( ph  ->  ( z  e.  {
0 ,  1 }  <-> 
( z  e.  {
0 ,  1 }  /\  ( z  =  0  \/  ph )
) ) )
8673, 85bitr4id 199 . . . . . . . . . 10  |-  ( ph  ->  ( z  e.  {
j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) }  <-> 
z  e.  { 0 ,  1 } ) )
8786eqrdv 2191 . . . . . . . . 9  |-  ( ph  ->  { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) }  =  { 0 ,  1 } )
8887supeq1d 7046 . . . . . . . 8  |-  ( ph  ->  sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  =  sup ( { 0 ,  1 } ,  RR ,  <  ) )
893a1i 9 . . . . . . . . . 10  |-  ( T. 
->  1  e.  RR )
903elexi 2772 . . . . . . . . . . . 12  |-  1  e.  _V
9190prid2 3725 . . . . . . . . . . 11  |-  1  e.  { 0 ,  1 }
9291a1i 9 . . . . . . . . . 10  |-  ( T. 
->  1  e.  { 0 ,  1 } )
93 elpri 3641 . . . . . . . . . . . 12  |-  ( z  e.  { 0 ,  1 }  ->  (
z  =  0  \/  z  =  1 ) )
942, 3lenlti 8120 . . . . . . . . . . . . . . 15  |-  ( 0  <_  1  <->  -.  1  <  0 )
9529, 94mpbi 145 . . . . . . . . . . . . . 14  |-  -.  1  <  0
96 breq2 4033 . . . . . . . . . . . . . 14  |-  ( z  =  0  ->  (
1  <  z  <->  1  <  0 ) )
9795, 96mtbiri 676 . . . . . . . . . . . . 13  |-  ( z  =  0  ->  -.  1  <  z )
98 breq2 4033 . . . . . . . . . . . . . 14  |-  ( z  =  1  ->  (
1  <  z  <->  1  <  1 ) )
9983, 98mtbiri 676 . . . . . . . . . . . . 13  |-  ( z  =  1  ->  -.  1  <  z )
10097, 99jaoi 717 . . . . . . . . . . . 12  |-  ( ( z  =  0  \/  z  =  1 )  ->  -.  1  <  z )
10193, 100syl 14 . . . . . . . . . . 11  |-  ( z  e.  { 0 ,  1 }  ->  -.  1  <  z )
102101adantl 277 . . . . . . . . . 10  |-  ( ( T.  /\  z  e. 
{ 0 ,  1 } )  ->  -.  1  <  z )
1035, 89, 92, 102supmaxti 7063 . . . . . . . . 9  |-  ( T. 
->  sup ( { 0 ,  1 } ,  RR ,  <  )  =  1 )
104103mptru 1373 . . . . . . . 8  |-  sup ( { 0 ,  1 } ,  RR ,  <  )  =  1
10588, 104eqtrdi 2242 . . . . . . 7  |-  ( ph  ->  sup ( { j  e.  { 0 ,  1 }  |  ( j  =  0  \/ 
ph ) } ,  RR ,  <  )  =  1 )
106105breq1d 4039 . . . . . 6  |-  ( ph  ->  ( sup ( { j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } ,  RR ,  <  )  <  1  <->  1  <  1 ) )
10783, 106mtbiri 676 . . . . 5  |-  ( ph  ->  -.  sup ( { j  e.  { 0 ,  1 }  | 
( j  =  0  \/  ph ) } ,  RR ,  <  )  <  1 )
108107con2i 628 . . . 4  |-  ( sup ( { j  e. 
{ 0 ,  1 }  |  ( j  =  0  \/  ph ) } ,  RR ,  <  )  <  1  ->  -.  ph )
10982, 108orim12i 760 . . 3  |-  ( ( 0  <  sup ( { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } ,  RR ,  <  )  \/  sup ( { j  e.  {
0 ,  1 }  |  ( j  =  0  \/  ph ) } ,  RR ,  <  )  <  1 )  ->  ( ph  \/  -.  ph ) )
11065, 109ax-mp 5 . 2  |-  ( ph  \/  -.  ph )
111 df-dc 836 . 2  |-  (DECID  ph  <->  ( ph  \/  -.  ph ) )
112110, 111mpbir 146 1  |- DECID  ph
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 709  DECID wdc 835    /\ w3a 980    = wceq 1364   T. wtru 1365   E.wex 1503    e. wcel 2164   A.wral 2472   E.wrex 2473   {crab 2476   _Vcvv 2760    C_ wss 3153   {cpr 3619   class class class wbr 4029   supcsup 7041   RRcr 7871   0cc0 7872   1c1 7873    < clt 8054    <_ cle 8055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1re 7966  ax-addrcl 7969  ax-0lt1 7978  ax-rnegex 7981  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-apti 7987
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rmo 2480  df-rab 2481  df-v 2762  df-sbc 2986  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-xp 4665  df-cnv 4667  df-iota 5215  df-riota 5873  df-sup 7043  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator