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

Theorem suplociccreex 13355
Description: An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7979 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 9899 . . . 4  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( B [,] C
)  C_  RR )
52, 3, 4syl2anc 409 . . 3  |-  ( ph  ->  ( B [,] C
)  C_  RR )
61, 5sstrd 3157 . 2  |-  ( ph  ->  A  C_  RR )
7 suplocicc.m . 2  |-  ( ph  ->  E. x  x  e.  A )
8 peano2re 8042 . . . 4  |-  ( C  e.  RR  ->  ( C  +  1 )  e.  RR )
93, 8syl 14 . . 3  |-  ( ph  ->  ( C  +  1 )  e.  RR )
106sselda 3147 . . . . 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 7956 . . . . . . 7  |-  ( ph  ->  B  e.  RR* )
1413adantr 274 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  B  e.  RR* )
153rexrd 7956 . . . . . . 7  |-  ( ph  ->  C  e.  RR* )
1615adantr 274 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  C  e.  RR* )
171sselda 3147 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  ( B [,] C
) )
18 iccleub 9875 . . . . . 6  |-  ( ( B  e.  RR*  /\  C  e.  RR*  /\  y  e.  ( B [,] C
) )  ->  y  <_  C )
1914, 16, 17, 18syl3anc 1233 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  y  <_  C )
2011ltp1d 8833 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  C  <  ( C  +  1 ) )
2110, 11, 12, 19, 20lelttrd 8031 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  y  <  ( C  +  1 ) )
2221ralrimiva 2543 . . 3  |-  ( ph  ->  A. y  e.  A  y  <  ( C  + 
1 ) )
23 brralrspcev 4045 . . 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 409 . 2  |-  ( ph  ->  E. x  e.  RR  A. y  e.  A  y  <  x )
257ad5antr 493 . . . . . . . . . 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 537 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  u  e.  RR )
2827ad2antrr 485 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  u  e.  RR )
292ad4antr 491 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  B  e.  RR )
3029ad2antrr 485 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  B  e.  RR )
316ad6antr 495 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  A  C_  RR )
3231, 26sseldd 3148 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  x  e.  RR )
33 simplr 525 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  u  <  B )
3413ad6antr 495 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  B  e.  RR* )
3515ad6antr 495 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  C  e.  RR* )
361ad6antr 495 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  A  C_  ( B [,] C
) )
3736, 26sseldd 3148 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  x  e.  ( B [,] C
) )
38 iccgelb 9876 . . . . . . . . . . . . . 14  |-  ( ( B  e.  RR*  /\  C  e.  RR*  /\  x  e.  ( B [,] C
) )  ->  B  <_  x )
3934, 35, 37, 38syl3anc 1233 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  B  <_  x )
4028, 30, 32, 33, 39ltletrd 8329 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  u  <  x )
41 breq2 3991 . . . . . . . . . . . . 13  |-  ( z  =  x  ->  (
u  <  z  <->  u  <  x ) )
4241rspcev 2834 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  u  <  x )  ->  E. z  e.  A  u  <  z )
4326, 40, 42syl2anc 409 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  u  <  B )  /\  x  e.  A )  ->  E. z  e.  A  u  <  z )
4443orcd 728 . . . . . . . . . 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 1891 . . . . . . . . 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 529 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  u  <  v )
47 simplr 525 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  u  <  C )
48 simp-5r 539 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  u  e.  RR )
49 simp-4r 537 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  v  e.  RR )
503ad5antr 493 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  C  e.  RR )
51 ltmininf 11185 . . . . . . . . . . . . . 14  |-  ( ( u  e.  RR  /\  v  e.  RR  /\  C  e.  RR )  ->  (
u  < inf ( {
v ,  C } ,  RR ,  <  )  <->  ( u  <  v  /\  u  <  C ) ) )
5248, 49, 50, 51syl3anc 1233 . . . . . . . . . . . . 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 939 . . . . . . . . . . . 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 493 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  <  C )
572ad5antr 493 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  e.  RR )
58 ltmininf 11185 . . . . . . . . . . . . . 14  |-  ( ( B  e.  RR  /\  v  e.  RR  /\  C  e.  RR )  ->  ( B  < inf ( { v ,  C } ,  RR ,  <  )  <->  ( B  <  v  /\  B  < 
C ) ) )
5957, 49, 50, 58syl3anc 1233 . . . . . . . . . . . . 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 939 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  < inf ( { v ,  C } ,  RR ,  <  ) )
61 mincl 11181 . . . . . . . . . . . . . 14  |-  ( ( v  e.  RR  /\  C  e.  RR )  -> inf ( { v ,  C } ,  RR ,  <  )  e.  RR )
6249, 50, 61syl2anc 409 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  -> inf ( { v ,  C } ,  RR ,  <  )  e.  RR )
63 maxltsup 11169 . . . . . . . . . . . . 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 1233 . . . . . . . . . . . 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 939 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  < inf ( {
v ,  C } ,  RR ,  <  )
)
66 breq2 3991 . . . . . . . . . . . . 13  |-  ( y  = inf ( { v ,  C } ,  RR ,  <  )  -> 
( sup ( { u ,  B } ,  RR ,  <  )  <  y  <->  sup ( { u ,  B } ,  RR ,  <  )  < inf ( { v ,  C } ,  RR ,  <  ) ) )
67 breq2 3991 . . . . . . . . . . . . . . 15  |-  ( y  = inf ( { v ,  C } ,  RR ,  <  )  -> 
( z  <  y  <->  z  < inf ( { v ,  C } ,  RR ,  <  ) ) )
6867ralbidv 2470 . . . . . . . . . . . . . 14  |-  ( y  = inf ( { v ,  C } ,  RR ,  <  )  -> 
( A. z  e.  A  z  <  y  <->  A. z  e.  A  z  < inf ( { v ,  C } ,  RR ,  <  ) ) )
6968orbi2d 785 . . . . . . . . . . . . 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 3990 . . . . . . . . . . . . . . 15  |-  ( x  =  sup ( { u ,  B } ,  RR ,  <  )  ->  ( x  <  y  <->  sup ( { u ,  B } ,  RR ,  <  )  <  y
) )
72 breq1 3990 . . . . . . . . . . . . . . . . 17  |-  ( x  =  sup ( { u ,  B } ,  RR ,  <  )  ->  ( x  <  z  <->  sup ( { u ,  B } ,  RR ,  <  )  <  z
) )
7372rexbidv 2471 . . . . . . . . . . . . . . . 16  |-  ( x  =  sup ( { u ,  B } ,  RR ,  <  )  ->  ( E. z  e.  A  x  <  z  <->  E. z  e.  A  sup ( { u ,  B } ,  RR ,  <  )  <  z ) )
7473orbi1d 786 . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . 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 493 . . . . . . . . . . . . 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 11161 . . . . . . . . . . . . . . 15  |-  ( ( u  e.  RR  /\  B  e.  RR )  ->  sup ( { u ,  B } ,  RR ,  <  )  e.  RR )
8048, 57, 79syl2anc 409 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  e.  RR )
81 maxle2 11163 . . . . . . . . . . . . . . 15  |-  ( ( u  e.  RR  /\  B  e.  RR )  ->  B  <_  sup ( { u ,  B } ,  RR ,  <  ) )
8248, 57, 81syl2anc 409 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  <_  sup ( { u ,  B } ,  RR ,  <  ) )
83 maxltsup 11169 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  ( sup ( { u ,  B } ,  RR ,  <  )  <  C  <->  ( u  <  C  /\  B  <  C ) ) )
8448, 57, 50, 83syl3anc 1233 . . . . . . . . . . . . . . . 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 939 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  <  C )
8680, 50, 85ltled 8025 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  <_  C )
87 elicc2 9882 . . . . . . . . . . . . . . 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 409 . . . . . . . . . . . . . 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 1175 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  sup ( { u ,  B } ,  RR ,  <  )  e.  ( B [,] C ) )
9076, 78, 89rspcdva 2839 . . . . . . . . . . . 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 8025 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  ->  B  <_ inf ( { v ,  C } ,  RR ,  <  ) )
92 min2inf 11183 . . . . . . . . . . . . . 14  |-  ( ( v  e.  RR  /\  C  e.  RR )  -> inf ( { v ,  C } ,  RR ,  <  )  <_  C
)
9349, 50, 92syl2anc 409 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  -> inf ( { v ,  C } ,  RR ,  <  )  <_  C )
94 elicc2 9882 . . . . . . . . . . . . . 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 409 . . . . . . . . . . . . 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 1175 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  u  <  C )  /\  B  <  v )  -> inf ( { v ,  C } ,  RR ,  <  )  e.  ( B [,] C
) )
9770, 90, 96rspcdva 2839 . . . . . . . . . . 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 485 . . . . . . . . . . . . . 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 525 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  u  e.  RR )
1012ad2antrr 485 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  B  e.  RR )
102100, 101, 79syl2anc 409 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  sup ( { u ,  B } ,  RR ,  <  )  e.  RR )
103102ad5antr 493 . . . . . . . . . . . . . 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 495 . . . . . . . . . . . . . . . 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 3148 . . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . 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 11162 . . . . . . . . . . . . . . 15  |-  ( ( u  e.  RR  /\  B  e.  RR )  ->  u  <_  sup ( { u ,  B } ,  RR ,  <  ) )
11099, 108, 109syl2anc 409 . . . . . . . . . . . . . 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 8031 . . . . . . . . . . . . 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 2572 . . . . . . . . . . 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 485 . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  ->  C  e.  RR )
121 min1inf 11182 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  RR  /\  C  e.  RR )  -> inf ( { v ,  C } ,  RR ,  <  )  <_  v
)
122119, 120, 121syl2anc 409 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  -> inf ( { v ,  C } ,  RR ,  <  )  <_  v )
123122ad5antr 493 . . . . . . . . . . . . . 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 8329 . . . . . . . . . . . . 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 2537 . . . . . . . . . . 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 781 . . . . . . . . . 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 525 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  u  <  v )
130 simpllr 529 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  u  <  C )  ->  v  e.  RR )
131 axltwlin 7974 . . . . . . . . . . 11  |-  ( ( u  e.  RR  /\  v  e.  RR  /\  B  e.  RR )  ->  (
u  <  v  ->  ( u  <  B  \/  B  <  v ) ) )
13227, 130, 29, 131syl3anc 1233 . . . . . . . . . 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 793 . . . . . . . 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 493 . . . . . . . . . . . 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 3148 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  z  e.  RR )
1383ad5antr 493 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  C  e.  RR )
139 simp-4r 537 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  v  e.  RR )
14013ad5antr 493 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  B  e.  RR* )
14115ad5antr 493 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  C  e.  RR* )
1421ad5antr 493 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  A  C_  ( B [,] C
) )
143142, 136sseldd 3148 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  z  e.  ( B [,] C
) )
144 iccleub 9875 . . . . . . . . . . . 12  |-  ( ( B  e.  RR*  /\  C  e.  RR*  /\  z  e.  ( B [,] C
) )  ->  z  <_  C )
145140, 141, 143, 144syl3anc 1233 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  z  <_  C )
146 simplr 525 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  C  <  v )
147137, 138, 139, 145, 146lelttrd 8031 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v )  /\  C  <  v )  /\  z  e.  A )  ->  z  <  v )
148147ralrimiva 2543 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  u  e.  RR )  /\  v  e.  RR )  /\  u  <  v
)  /\  C  <  v )  ->  A. z  e.  A  z  <  v )
149148olcd 729 . . . . . . . 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 7974 . . . . . . . . . 10  |-  ( ( u  e.  RR  /\  v  e.  RR  /\  C  e.  RR )  ->  (
u  <  v  ->  ( u  <  C  \/  C  <  v ) ) )
151100, 119, 120, 150syl3anc 1233 . . . . . . . . 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 793 . . . . . . 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 2543 . . . . 5  |-  ( (
ph  /\  u  e.  RR )  ->  A. v  e.  RR  ( u  < 
v  ->  ( E. z  e.  A  u  <  z  \/  A. z  e.  A  z  <  v ) ) )
156155ralrimiva 2543 . . . 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 3991 . . . . . . 7  |-  ( v  =  y  ->  (
u  <  v  <->  u  <  y ) )
158 breq2 3991 . . . . . . . . 9  |-  ( v  =  y  ->  (
z  <  v  <->  z  <  y ) )
159158ralbidv 2470 . . . . . . . 8  |-  ( v  =  y  ->  ( A. z  e.  A  z  <  v  <->  A. z  e.  A  z  <  y ) )
160159orbi2d 785 . . . . . . 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 2696 . . . . 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 2476 . . . 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 3990 . . . . . 6  |-  ( u  =  x  ->  (
u  <  y  <->  x  <  y ) )
166 breq1 3990 . . . . . . . 8  |-  ( u  =  x  ->  (
u  <  z  <->  x  <  z ) )
167166rexbidv 2471 . . . . . . 7  |-  ( u  =  x  ->  ( E. z  e.  A  u  <  z  <->  E. z  e.  A  x  <  z ) )
168167orbi1d 786 . . . . . 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 2470 . . . 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 2696 . . 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 7979 . 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 1234 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 703    /\ w3a 973    = wceq 1348   E.wex 1485    e. wcel 2141   A.wral 2448   E.wrex 2449    C_ wss 3121   {cpr 3582   class class class wbr 3987  (class class class)co 5850   supcsup 6955  infcinf 6956   RRcr 7760   1c1 7762    + caddc 7764   RR*cxr 7940    < clt 7941    <_ cle 7942   [,]cicc 9835
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-nul 4113  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-iinf 4570  ax-cnex 7852  ax-resscn 7853  ax-1cn 7854  ax-1re 7855  ax-icn 7856  ax-addcl 7857  ax-addrcl 7858  ax-mulcl 7859  ax-mulrcl 7860  ax-addcom 7861  ax-mulcom 7862  ax-addass 7863  ax-mulass 7864  ax-distr 7865  ax-i2m1 7866  ax-0lt1 7867  ax-1rid 7868  ax-0id 7869  ax-rnegex 7870  ax-precex 7871  ax-cnre 7872  ax-pre-ltirr 7873  ax-pre-ltwlin 7874  ax-pre-lttrn 7875  ax-pre-apti 7876  ax-pre-ltadd 7877  ax-pre-mulgt0 7878  ax-pre-mulext 7879  ax-arch 7880  ax-caucvg 7881  ax-pre-suploc 7882
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3526  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-tr 4086  df-id 4276  df-po 4279  df-iso 4280  df-iord 4349  df-on 4351  df-ilim 4352  df-suc 4354  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-isom 5205  df-riota 5806  df-ov 5853  df-oprab 5854  df-mpo 5855  df-1st 6116  df-2nd 6117  df-recs 6281  df-frec 6367  df-sup 6957  df-inf 6958  df-pnf 7943  df-mnf 7944  df-xr 7945  df-ltxr 7946  df-le 7947  df-sub 8079  df-neg 8080  df-reap 8481  df-ap 8488  df-div 8577  df-inn 8866  df-2 8924  df-3 8925  df-4 8926  df-n0 9123  df-z 9200  df-uz 9475  df-rp 9598  df-icc 9839  df-seqfrec 10389  df-exp 10463  df-cj 10793  df-re 10794  df-im 10795  df-rsqrt 10949  df-abs 10950
This theorem is referenced by:  suplociccex  13356
  Copyright terms: Public domain W3C validator