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

Theorem suplociccreex 12780
Description: An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7844 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
Hypotheses
Ref Expression
suplocicc.1  |-  ( ph  ->  B  e.  RR )
suplocicc.2  |-  ( ph  ->  C  e.  RR )
suplocicc.bc  |-  ( ph  ->  B  <  C )
suplocicc.3  |-  ( ph  ->  A  C_  ( B [,] C ) )
suplocicc.m  |-  ( ph  ->  E. x  x  e.  A )
suplocicc.l  |-  ( ph  ->  A. x  e.  ( B [,] C ) A. y  e.  ( B [,] C ) ( x  <  y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )
Assertion
Ref Expression
suplociccreex  |-  ( ph  ->  E. x  e.  RR  ( A. y  e.  A  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  A  y  <  z ) ) )
Distinct variable groups:    x, A, y, z    x, B, y, z    x, C, y, z    ph, x, y, z

Proof of Theorem suplociccreex
Dummy variables  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suplocicc.3 . . 3  |-  ( ph  ->  A  C_  ( B [,] C ) )
2 suplocicc.1 . . . 4  |-  ( ph  ->  B  e.  RR )
3 suplocicc.2 . . . 4  |-  ( ph  ->  C  e.  RR )
4 iccssre 9745 . . . 4  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( B [,] C
)  C_  RR )
52, 3, 4syl2anc 408 . . 3  |-  ( ph  ->  ( B [,] C
)  C_  RR )
61, 5sstrd 3107 . 2  |-  ( ph  ->  A  C_  RR )
7 suplocicc.m . 2  |-  ( ph  ->  E. x  x  e.  A )
8 peano2re 7905 . . . 4  |-  ( C  e.  RR  ->  ( C  +  1 )  e.  RR )
93, 8syl 14 . . 3  |-  ( ph  ->  ( C  +  1 )  e.  RR )
106sselda 3097 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  RR )
113adantr 274 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  C  e.  RR )
129adantr 274 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  ( C  +  1 )  e.  RR )
132rexrd 7822 . . . . . . 7  |-  ( ph  ->  B  e.  RR* )
1413adantr 274 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  B  e.  RR* )
153rexrd 7822 . . . . . . 7  |-  ( ph  ->  C  e.  RR* )
1615adantr 274 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  C  e.  RR* )
171sselda 3097 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  ( B [,] C
) )
18 iccleub 9721 . . . . . 6  |-  ( ( B  e.  RR*  /\  C  e.  RR*  /\  y  e.  ( B [,] C
) )  ->  y  <_  C )
1914, 16, 17, 18syl3anc 1216 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  y  <_  C )
2011ltp1d 8695 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  C  <  ( C  +  1 ) )
2110, 11, 12, 19, 20lelttrd 7894 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  y  <  ( C  +  1 ) )
2221ralrimiva 2505 . . 3  |-  ( ph  ->  A. y  e.  A  y  <  ( C  + 
1 ) )
23 brralrspcev 3986 . . 3  |-  ( ( ( C  +  1 )  e.  RR  /\  A. y  e.  A  y  <  ( C  + 
1 ) )  ->  E. x  e.  RR  A. y  e.  A  y  <  x )
249, 22, 23syl2anc 408 . 2  |-  ( ph  ->  E. x  e.  RR  A. y  e.  A  y  <  x )
257ad5antr 487 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  ->  E. x  x  e.  A )
26 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  x  e.  A )
27 simp-4r 531 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  u  e.  RR )
2827ad2antrr 479 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  u  e.  RR )
292ad4antr 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  B  e.  RR )
3029ad2antrr 479 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  B  e.  RR )
316ad6antr 489 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  A  C_  RR )
3231, 26sseldd 3098 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  x  e.  RR )
33 simplr 519 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  u  <  B )
3413ad6antr 489 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  B  e.  RR* )
3515ad6antr 489 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  C  e.  RR* )
361ad6antr 489 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  A  C_  ( B [,] C
) )
3736, 26sseldd 3098 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  x  e.  ( B [,] C
) )
38 iccgelb 9722 . . . . . . . . . . . . . 14  |-  ( ( B  e.  RR*  /\  C  e.  RR*  /\  x  e.  ( B [,] C
) )  ->  B  <_  x )
3934, 35, 37, 38syl3anc 1216 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  B  <_  x )
4028, 30, 32, 33, 39ltletrd 8192 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  u  <  x )
41 breq2 3933 . . . . . . . . . . . . 13  |-  ( z  =  x  ->  (
u  <  z  <->  u  <  x ) )
4241rspcev 2789 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  u  <  x )  ->  E. z  e.  A  u  <  z )
4326, 40, 42syl2anc 408 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  E. z  e.  A  u  <  z )
4443orcd 722 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) )
4525, 44exlimddv 1870 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) )
46 simpllr 523 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  u  <  v )
47 simplr 519 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  u  <  C )
48 simp-5r 533 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  u  e.  RR )
49 simp-4r 531 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  v  e.  RR )
503ad5antr 487 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  C  e.  RR )
51 ltmininf 11013 . . . . . . . . . . . . . 14  |-  ( ( u  e.  RR  /\  v  e.  RR  /\  C  e.  RR )  ->  (
u  < inf ( {
v ,  C } ,  RR ,  <  )  <->  ( u  <  v  /\  u  <  C ) ) )
5248, 49, 50, 51syl3anc 1216 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  (
u  < inf ( {
v ,  C } ,  RR ,  <  )  <->  ( u  <  v  /\  u  <  C ) ) )
5346, 47, 52mpbir2and 928 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  u  < inf ( { v ,  C } ,  RR ,  <  ) )
54 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  <  v )
55 suplocicc.bc . . . . . . . . . . . . . 14  |-  ( ph  ->  B  <  C )
5655ad5antr 487 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  <  C )
572ad5antr 487 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  e.  RR )
58 ltmininf 11013 . . . . . . . . . . . . . 14  |-  ( ( B  e.  RR  /\  v  e.  RR  /\  C  e.  RR )  ->  ( B  < inf ( { v ,  C } ,  RR ,  <  )  <->  ( B  <  v  /\  B  < 
C ) ) )
5957, 49, 50, 58syl3anc 1216 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  ( B  < inf ( { v ,  C } ,  RR ,  <  )  <->  ( B  <  v  /\  B  < 
C ) ) )
6054, 56, 59mpbir2and 928 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  < inf ( { v ,  C } ,  RR ,  <  ) )
61 mincl 11009 . . . . . . . . . . . . . 14  |-  ( ( v  e.  RR  /\  C  e.  RR )  -> inf ( { v ,  C } ,  RR ,  <  )  e.  RR )
6249, 50, 61syl2anc 408 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  -> inf ( { v ,  C } ,  RR ,  <  )  e.  RR )
63 maxltsup 10997 . . . . . . . . . . . . 13  |-  ( ( u  e.  RR  /\  B  e.  RR  /\ inf ( { v ,  C } ,  RR ,  <  )  e.  RR )  ->  ( sup ( { u ,  B } ,  RR ,  <  )  < inf ( {
v ,  C } ,  RR ,  <  )  <->  ( u  < inf ( {
v ,  C } ,  RR ,  <  )  /\  B  < inf ( { v ,  C } ,  RR ,  <  )
) ) )
6448, 57, 62, 63syl3anc 1216 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  ( sup ( { u ,  B } ,  RR ,  <  )  < inf ( { v ,  C } ,  RR ,  <  )  <->  ( u  < inf ( { v ,  C } ,  RR ,  <  )  /\  B  < inf ( { v ,  C } ,  RR ,  <  ) ) ) )
6553, 60, 64mpbir2and 928 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  < inf ( {
v ,  C } ,  RR ,  <  )
)
66 breq2 3933 . . . . . . . . . . . . 13  |-  ( y  = inf ( { v ,  C } ,  RR ,  <  )  -> 
( sup ( { u ,  B } ,  RR ,  <  )  <  y  <->  sup ( { u ,  B } ,  RR ,  <  )  < inf ( { v ,  C } ,  RR ,  <  ) ) )
67 breq2 3933 . . . . . . . . . . . . . . 15  |-  ( y  = inf ( { v ,  C } ,  RR ,  <  )  -> 
( z  <  y  <->  z  < inf ( { v ,  C } ,  RR ,  <  ) ) )
6867ralbidv 2437 . . . . . . . . . . . . . 14  |-  ( y  = inf ( { v ,  C } ,  RR ,  <  )  -> 
( A. z  e.  A  z  <  y  <->  A. z  e.  A  z  < inf ( { v ,  C } ,  RR ,  <  ) ) )
6968orbi2d 779 . . . . . . . . . . . . 13  |-  ( y  = inf ( { v ,  C } ,  RR ,  <  )  -> 
( ( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/ 
A. z  e.  A  z  <  y )  <->  ( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/ 
A. z  e.  A  z  < inf ( { v ,  C } ,  RR ,  <  ) ) ) )
7066, 69imbi12d 233 . . . . . . . . . . . 12  |-  ( y  = inf ( { v ,  C } ,  RR ,  <  )  -> 
( ( sup ( { u ,  B } ,  RR ,  <  )  <  y  -> 
( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/  A. z  e.  A  z  <  y ) )  <->  ( sup ( { u ,  B } ,  RR ,  <  )  < inf ( {
v ,  C } ,  RR ,  <  )  ->  ( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/  A. z  e.  A  z  < inf ( { v ,  C } ,  RR ,  <  ) ) ) ) )
71 breq1 3932 . . . . . . . . . . . . . . 15  |-  ( x  =  sup ( { u ,  B } ,  RR ,  <  )  ->  ( x  <  y  <->  sup ( { u ,  B } ,  RR ,  <  )  <  y
) )
72 breq1 3932 . . . . . . . . . . . . . . . . 17  |-  ( x  =  sup ( { u ,  B } ,  RR ,  <  )  ->  ( x  <  z  <->  sup ( { u ,  B } ,  RR ,  <  )  <  z
) )
7372rexbidv 2438 . . . . . . . . . . . . . . . 16  |-  ( x  =  sup ( { u ,  B } ,  RR ,  <  )  ->  ( E. z  e.  A  x  <  z  <->  E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z ) )
7473orbi1d 780 . . . . . . . . . . . . . . 15  |-  ( x  =  sup ( { u ,  B } ,  RR ,  <  )  ->  ( ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y
)  <->  ( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/ 
A. z  e.  A  z  <  y ) ) )
7571, 74imbi12d 233 . . . . . . . . . . . . . 14  |-  ( x  =  sup ( { u ,  B } ,  RR ,  <  )  ->  ( ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) )  <->  ( sup ( { u ,  B } ,  RR ,  <  )  <  y  -> 
( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/  A. z  e.  A  z  <  y ) ) ) )
7675ralbidv 2437 . . . . . . . . . . . . 13  |-  ( x  =  sup ( { u ,  B } ,  RR ,  <  )  ->  ( A. y  e.  ( B [,] C
) ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) )  <->  A. y  e.  ( B [,] C
) ( sup ( { u ,  B } ,  RR ,  <  )  <  y  -> 
( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/  A. z  e.  A  z  <  y ) ) ) )
77 suplocicc.l . . . . . . . . . . . . . 14  |-  ( ph  ->  A. x  e.  ( B [,] C ) A. y  e.  ( B [,] C ) ( x  <  y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )
7877ad5antr 487 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  A. x  e.  ( B [,] C
) A. y  e.  ( B [,] C
) ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )
79 maxcl 10989 . . . . . . . . . . . . . . 15  |-  ( ( u  e.  RR  /\  B  e.  RR )  ->  sup ( { u ,  B } ,  RR ,  <  )  e.  RR )
8048, 57, 79syl2anc 408 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  e.  RR )
81 maxle2 10991 . . . . . . . . . . . . . . 15  |-  ( ( u  e.  RR  /\  B  e.  RR )  ->  B  <_  sup ( { u ,  B } ,  RR ,  <  ) )
8248, 57, 81syl2anc 408 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  <_  sup ( { u ,  B } ,  RR ,  <  ) )
83 maxltsup 10997 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( sup ( { u ,  B } ,  RR ,  <  )  <  C  <->  ( u  <  C  /\  B  <  C ) ) )
8448, 57, 50, 83syl3anc 1216 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  ( sup ( { u ,  B } ,  RR ,  <  )  <  C  <->  ( u  <  C  /\  B  <  C ) ) )
8547, 56, 84mpbir2and 928 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  <  C )
8680, 50, 85ltled 7888 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  <_  C )
87 elicc2 9728 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( sup ( { u ,  B } ,  RR ,  <  )  e.  ( B [,] C
)  <->  ( sup ( { u ,  B } ,  RR ,  <  )  e.  RR  /\  B  <_  sup ( { u ,  B } ,  RR ,  <  )  /\  sup ( { u ,  B } ,  RR ,  <  )  <_  C )
) )
8857, 50, 87syl2anc 408 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  ( sup ( { u ,  B } ,  RR ,  <  )  e.  ( B [,] C )  <-> 
( sup ( { u ,  B } ,  RR ,  <  )  e.  RR  /\  B  <_  sup ( { u ,  B } ,  RR ,  <  )  /\  sup ( { u ,  B } ,  RR ,  <  )  <_  C )
) )
8980, 82, 86, 88mpbir3and 1164 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  e.  ( B [,] C ) )
9076, 78, 89rspcdva 2794 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  A. y  e.  ( B [,] C
) ( sup ( { u ,  B } ,  RR ,  <  )  <  y  -> 
( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/  A. z  e.  A  z  <  y ) ) )
9157, 62, 60ltled 7888 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  <_ inf ( { v ,  C } ,  RR ,  <  ) )
92 min2inf 11011 . . . . . . . . . . . . . 14  |-  ( ( v  e.  RR  /\  C  e.  RR )  -> inf ( { v ,  C } ,  RR ,  <  )  <_  C
)
9349, 50, 92syl2anc 408 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  -> inf ( { v ,  C } ,  RR ,  <  )  <_  C )
94 elicc2 9728 . . . . . . . . . . . . . 14  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  (inf ( { v ,  C } ,  RR ,  <  )  e.  ( B [,] C
)  <->  (inf ( { v ,  C } ,  RR ,  <  )  e.  RR  /\  B  <_ inf ( { v ,  C } ,  RR ,  <  )  /\ inf ( {
v ,  C } ,  RR ,  <  )  <_  C ) ) )
9557, 50, 94syl2anc 408 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  (inf ( { v ,  C } ,  RR ,  <  )  e.  ( B [,] C )  <->  (inf ( { v ,  C } ,  RR ,  <  )  e.  RR  /\  B  <_ inf ( { v ,  C } ,  RR ,  <  )  /\ inf ( { v ,  C } ,  RR ,  <  )  <_  C )
) )
9662, 91, 93, 95mpbir3and 1164 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  -> inf ( { v ,  C } ,  RR ,  <  )  e.  ( B [,] C
) )
9770, 90, 96rspcdva 2794 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  ( sup ( { u ,  B } ,  RR ,  <  )  < inf ( { v ,  C } ,  RR ,  <  )  ->  ( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/ 
A. z  e.  A  z  < inf ( { v ,  C } ,  RR ,  <  ) ) ) )
9865, 97mpd 13 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  ( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/  A. z  e.  A  z  < inf ( { v ,  C } ,  RR ,  <  ) ) )
9948ad2antrr 479 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  sup ( { u ,  B } ,  RR ,  <  )  <  z )  ->  u  e.  RR )
100 simplr 519 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  u  e.  RR )
1012ad2antrr 479 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  B  e.  RR )
102100, 101, 79syl2anc 408 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  sup ( { u ,  B } ,  RR ,  <  )  e.  RR )
103102ad5antr 487 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  sup ( { u ,  B } ,  RR ,  <  )  <  z )  ->  sup ( { u ,  B } ,  RR ,  <  )  e.  RR )
1046ad6antr 489 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  /\  z  e.  A )  ->  A  C_  RR )
105 simpr 109 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  /\  z  e.  A )  ->  z  e.  A )
106104, 105sseldd 3098 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  /\  z  e.  A )  ->  z  e.  RR )
107106adantr 274 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  sup ( { u ,  B } ,  RR ,  <  )  <  z )  ->  z  e.  RR )
10857ad2antrr 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  sup ( { u ,  B } ,  RR ,  <  )  <  z )  ->  B  e.  RR )
109 maxle1 10990 . . . . . . . . . . . . . . 15  |-  ( ( u  e.  RR  /\  B  e.  RR )  ->  u  <_  sup ( { u ,  B } ,  RR ,  <  ) )
11099, 108, 109syl2anc 408 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  sup ( { u ,  B } ,  RR ,  <  )  <  z )  ->  u  <_  sup ( { u ,  B } ,  RR ,  <  ) )
111 simpr 109 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  sup ( { u ,  B } ,  RR ,  <  )  <  z )  ->  sup ( { u ,  B } ,  RR ,  <  )  <  z
)
11299, 103, 107, 110, 111lelttrd 7894 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  sup ( { u ,  B } ,  RR ,  <  )  <  z )  ->  u  <  z
)
113112ex 114 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  /\  z  e.  A )  ->  ( sup ( { u ,  B } ,  RR ,  <  )  <  z  ->  u  <  z ) )
114113reximdva 2534 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  ( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  ->  E. z  e.  A  u  <  z ) )
115106adantr 274 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  z  < inf ( { v ,  C } ,  RR ,  <  ) )  -> 
z  e.  RR )
11662ad2antrr 479 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  z  < inf ( { v ,  C } ,  RR ,  <  ) )  -> inf ( { v ,  C } ,  RR ,  <  )  e.  RR )
11749ad2antrr 479 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  z  < inf ( { v ,  C } ,  RR ,  <  ) )  -> 
v  e.  RR )
118 simpr 109 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  z  < inf ( { v ,  C } ,  RR ,  <  ) )  -> 
z  < inf ( {
v ,  C } ,  RR ,  <  )
)
119 simpr 109 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  v  e.  RR )
1203ad2antrr 479 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  C  e.  RR )
121 min1inf 11010 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  RR  /\  C  e.  RR )  -> inf ( { v ,  C } ,  RR ,  <  )  <_  v
)
122119, 120, 121syl2anc 408 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  -> inf ( { v ,  C } ,  RR ,  <  )  <_  v )
123122ad5antr 487 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  z  < inf ( { v ,  C } ,  RR ,  <  ) )  -> inf ( { v ,  C } ,  RR ,  <  )  <_  v )
124115, 116, 117, 118, 123ltletrd 8192 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  /\  B  < 
v )  /\  z  e.  A )  /\  z  < inf ( { v ,  C } ,  RR ,  <  ) )  -> 
z  <  v )
125124ex 114 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  /\  z  e.  A )  ->  (
z  < inf ( {
v ,  C } ,  RR ,  <  )  ->  z  <  v ) )
126125ralimdva 2499 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  ( A. z  e.  A  z  < inf ( { v ,  C } ,  RR ,  <  )  ->  A. z  e.  A  z  <  v ) )
127114, 126orim12d 775 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  (
( E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z  \/  A. z  e.  A  z  < inf ( { v ,  C } ,  RR ,  <  ) )  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) ) )
12898, 127mpd 13 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) )
129 simplr 519 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  u  <  v )
130 simpllr 523 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  v  e.  RR )
131 axltwlin 7839 . . . . . . . . . . 11  |-  ( ( u  e.  RR  /\  v  e.  RR  /\  B  e.  RR )  ->  (
u  <  v  ->  ( u  <  B  \/  B  <  v ) ) )
13227, 130, 29, 131syl3anc 1216 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  ( u  <  v  ->  ( u  <  B  \/  B  < 
v ) ) )
133129, 132mpd 13 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  ( u  <  B  \/  B  < 
v ) )
13445, 128, 133mpjaodan 787 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) )
1356ad5antr 487 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  A  C_  RR )
136 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  z  e.  A )
137135, 136sseldd 3098 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  z  e.  RR )
1383ad5antr 487 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  C  e.  RR )
139 simp-4r 531 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  v  e.  RR )
14013ad5antr 487 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  B  e.  RR* )
14115ad5antr 487 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  C  e.  RR* )
1421ad5antr 487 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  A  C_  ( B [,] C
) )
143142, 136sseldd 3098 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  z  e.  ( B [,] C
) )
144 iccleub 9721 . . . . . . . . . . . 12  |-  ( ( B  e.  RR*  /\  C  e.  RR*  /\  z  e.  ( B [,] C
) )  ->  z  <_  C )
145140, 141, 143, 144syl3anc 1216 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  z  <_  C )
146 simplr 519 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  C  <  v )
147137, 138, 139, 145, 146lelttrd 7894 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  z  <  v )
148147ralrimiva 2505 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  C  <  v )  ->  A. z  e.  A  z  <  v )
149148olcd 723 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  C  <  v )  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) )
150 axltwlin 7839 . . . . . . . . . 10  |-  ( ( u  e.  RR  /\  v  e.  RR  /\  C  e.  RR )  ->  (
u  <  v  ->  ( u  <  C  \/  C  <  v ) ) )
151100, 119, 120, 150syl3anc 1216 . . . . . . . . 9  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  (
u  <  v  ->  ( u  <  C  \/  C  <  v ) ) )
152151imp 123 . . . . . . . 8  |-  ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  ->  ( u  <  C  \/  C  < 
v ) )
153134, 149, 152mpjaodan 787 . . . . . . 7  |-  ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) )
154153ex 114 . . . . . 6  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  (
u  <  v  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) ) )
155154ralrimiva 2505 . . . . 5  |-  ( (
ph  /\  u  e.  RR )  ->  A. v  e.  RR  ( u  < 
v  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) ) )
156155ralrimiva 2505 . . . 4  |-  ( ph  ->  A. u  e.  RR  A. v  e.  RR  (
u  <  v  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) ) )
157 breq2 3933 . . . . . . 7  |-  ( v  =  y  ->  (
u  <  v  <->  u  <  y ) )
158 breq2 3933 . . . . . . . . 9  |-  ( v  =  y  ->  (
z  <  v  <->  z  <  y ) )
159158ralbidv 2437 . . . . . . . 8  |-  ( v  =  y  ->  ( A. z  e.  A  z  <  v  <->  A. z  e.  A  z  <  y ) )
160159orbi2d 779 . . . . . . 7  |-  ( v  =  y  ->  (
( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v )  <->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  y ) ) )
161157, 160imbi12d 233 . . . . . 6  |-  ( v  =  y  ->  (
( u  <  v  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) )  <-> 
( u  <  y  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  y ) ) ) )
162161cbvralv 2654 . . . . 5  |-  ( A. v  e.  RR  (
u  <  v  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) )  <->  A. y  e.  RR  ( u  < 
y  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  y ) ) )
163162ralbii 2441 . . . 4  |-  ( A. u  e.  RR  A. v  e.  RR  ( u  < 
v  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) )  <->  A. u  e.  RR  A. y  e.  RR  ( u  < 
y  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  y ) ) )
164156, 163sylib 121 . . 3  |-  ( ph  ->  A. u  e.  RR  A. y  e.  RR  (
u  <  y  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  y ) ) )
165 breq1 3932 . . . . . 6  |-  ( u  =  x  ->  (
u  <  y  <->  x  <  y ) )
166 breq1 3932 . . . . . . . 8  |-  ( u  =  x  ->  (
u  <  z  <->  x  <  z ) )
167166rexbidv 2438 . . . . . . 7  |-  ( u  =  x  ->  ( E. z  e.  A  u  <  z  <->  E. z  e.  A  x  <  z ) )
168167orbi1d 780 . . . . . 6  |-  ( u  =  x  ->  (
( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  y )  <->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )
169165, 168imbi12d 233 . . . . 5  |-  ( u  =  x  ->  (
( u  <  y  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  y ) )  <-> 
( x  <  y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) ) )
170169ralbidv 2437 . . . 4  |-  ( u  =  x  ->  ( A. y  e.  RR  ( u  <  y  -> 
( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  y ) )  <->  A. y  e.  RR  ( x  <  y  -> 
( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) ) )
171170cbvralv 2654 . . 3  |-  ( A. u  e.  RR  A. y  e.  RR  ( u  < 
y  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  y ) )  <->  A. x  e.  RR  A. y  e.  RR  ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )
172164, 171sylib 121 . 2  |-  ( ph  ->  A. x  e.  RR  A. y  e.  RR  (
x  <  y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )
173 axsuploc 7844 . 2  |-  ( ( ( A  C_  RR  /\ 
E. x  x  e.  A )  /\  ( E. x  e.  RR  A. y  e.  A  y  <  x  /\  A. x  e.  RR  A. y  e.  RR  ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) ) )  ->  E. x  e.  RR  ( A. y  e.  A  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  A  y  <  z ) ) )
1746, 7, 24, 172, 173syl22anc 1217 1  |-  ( ph  ->  E. x  e.  RR  ( A. y  e.  A  -.  x  <  y  /\  A. y  e.  RR  (
y  <  x  ->  E. z  e.  A  y  <  z ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 697    /\ w3a 962    = wceq 1331   E.wex 1468    e. wcel 1480   A.wral 2416   E.wrex 2417    C_ wss 3071   {cpr 3528   class class class wbr 3929  (class class class)co 5774   supcsup 6869  infcinf 6870   RRcr 7626   1c1 7628    + caddc 7630   RR*cxr 7806    < clt 7807    <_ cle 7808   [,]cicc 9681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7718  ax-resscn 7719  ax-1cn 7720  ax-1re 7721  ax-icn 7722  ax-addcl 7723  ax-addrcl 7724  ax-mulcl 7725  ax-mulrcl 7726  ax-addcom 7727  ax-mulcom 7728  ax-addass 7729  ax-mulass 7730  ax-distr 7731  ax-i2m1 7732  ax-0lt1 7733  ax-1rid 7734  ax-0id 7735  ax-rnegex 7736  ax-precex 7737  ax-cnre 7738  ax-pre-ltirr 7739  ax-pre-ltwlin 7740  ax-pre-lttrn 7741  ax-pre-apti 7742  ax-pre-ltadd 7743  ax-pre-mulgt0 7744  ax-pre-mulext 7745  ax-arch 7746  ax-caucvg 7747  ax-pre-suploc 7748
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-isom 5132  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-sup 6871  df-inf 6872  df-pnf 7809  df-mnf 7810  df-xr 7811  df-ltxr 7812  df-le 7813  df-sub 7942  df-neg 7943  df-reap 8344  df-ap 8351  df-div 8440  df-inn 8728  df-2 8786  df-3 8787  df-4 8788  df-n0 8985  df-z 9062  df-uz 9334  df-rp 9449  df-icc 9685  df-seqfrec 10226  df-exp 10300  df-cj 10621  df-re 10622  df-im 10623  df-rsqrt 10777  df-abs 10778
This theorem is referenced by:  suplociccex  12781
  Copyright terms: Public domain W3C validator