MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reconnlem2 Structured version   Unicode version

Theorem reconnlem2 21067
Description: Lemma for reconn 21068. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)
Hypotheses
Ref Expression
reconnlem2.1  |-  ( ph  ->  A  C_  RR )
reconnlem2.2  |-  ( ph  ->  U  e.  ( topGen ` 
ran  (,) ) )
reconnlem2.3  |-  ( ph  ->  V  e.  ( topGen ` 
ran  (,) ) )
reconnlem2.4  |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x [,] y
)  C_  A )
reconnlem2.5  |-  ( ph  ->  B  e.  ( U  i^i  A ) )
reconnlem2.6  |-  ( ph  ->  C  e.  ( V  i^i  A ) )
reconnlem2.7  |-  ( ph  ->  ( U  i^i  V
)  C_  ( RR  \  A ) )
reconnlem2.8  |-  ( ph  ->  B  <_  C )
reconnlem2.9  |-  S  =  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )
Assertion
Ref Expression
reconnlem2  |-  ( ph  ->  -.  A  C_  ( U  u.  V )
)
Distinct variable groups:    x, y, A    x, B, y    y, C
Allowed substitution hints:    ph( x, y)    C( x)    S( x, y)    U( x, y)    V( x, y)

Proof of Theorem reconnlem2
Dummy variables  w  z  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reconnlem2.9 . . . . . . . . . . 11  |-  S  =  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )
2 inss2 3719 . . . . . . . . . . . . 13  |-  ( U  i^i  ( B [,] C ) )  C_  ( B [,] C )
3 inss2 3719 . . . . . . . . . . . . . . . 16  |-  ( U  i^i  A )  C_  A
4 reconnlem2.5 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  B  e.  ( U  i^i  A ) )
53, 4sseldi 3502 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  A )
6 inss2 3719 . . . . . . . . . . . . . . . 16  |-  ( V  i^i  A )  C_  A
7 reconnlem2.6 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  ( V  i^i  A ) )
86, 7sseldi 3502 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  A )
9 reconnlem2.4 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x [,] y
)  C_  A )
10 oveq1 6289 . . . . . . . . . . . . . . . . 17  |-  ( x  =  B  ->  (
x [,] y )  =  ( B [,] y ) )
1110sseq1d 3531 . . . . . . . . . . . . . . . 16  |-  ( x  =  B  ->  (
( x [,] y
)  C_  A  <->  ( B [,] y )  C_  A
) )
12 oveq2 6290 . . . . . . . . . . . . . . . . 17  |-  ( y  =  C  ->  ( B [,] y )  =  ( B [,] C
) )
1312sseq1d 3531 . . . . . . . . . . . . . . . 16  |-  ( y  =  C  ->  (
( B [,] y
)  C_  A  <->  ( B [,] C )  C_  A
) )
1411, 13rspc2va 3224 . . . . . . . . . . . . . . 15  |-  ( ( ( B  e.  A  /\  C  e.  A
)  /\  A. x  e.  A  A. y  e.  A  ( x [,] y )  C_  A
)  ->  ( B [,] C )  C_  A
)
155, 8, 9, 14syl21anc 1227 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B [,] C
)  C_  A )
16 reconnlem2.1 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  RR )
1715, 16sstrd 3514 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B [,] C
)  C_  RR )
182, 17syl5ss 3515 . . . . . . . . . . . 12  |-  ( ph  ->  ( U  i^i  ( B [,] C ) ) 
C_  RR )
19 inss1 3718 . . . . . . . . . . . . . . 15  |-  ( U  i^i  A )  C_  U
2019, 4sseldi 3502 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  U )
2116, 5sseldd 3505 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  B  e.  RR )
2221rexrd 9639 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  RR* )
2316, 8sseldd 3505 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR )
2423rexrd 9639 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  RR* )
25 reconnlem2.8 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  <_  C )
26 lbicc2 11632 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  RR*  /\  C  e.  RR*  /\  B  <_  C )  ->  B  e.  ( B [,] C
) )
2722, 24, 25, 26syl3anc 1228 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  ( B [,] C ) )
2820, 27elind 3688 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  ( U  i^i  ( B [,] C ) ) )
29 ne0i 3791 . . . . . . . . . . . . 13  |-  ( B  e.  ( U  i^i  ( B [,] C ) )  ->  ( U  i^i  ( B [,] C
) )  =/=  (/) )
3028, 29syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( U  i^i  ( B [,] C ) )  =/=  (/) )
312sseli 3500 . . . . . . . . . . . . . . 15  |-  ( w  e.  ( U  i^i  ( B [,] C ) )  ->  w  e.  ( B [,] C ) )
32 elicc2 11585 . . . . . . . . . . . . . . . . 17  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( w  e.  ( B [,] C )  <-> 
( w  e.  RR  /\  B  <_  w  /\  w  <_  C ) ) )
3321, 23, 32syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( w  e.  ( B [,] C )  <-> 
( w  e.  RR  /\  B  <_  w  /\  w  <_  C ) ) )
34 simp3 998 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  RR  /\  B  <_  w  /\  w  <_  C )  ->  w  <_  C )
3533, 34syl6bi 228 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( w  e.  ( B [,] C )  ->  w  <_  C
) )
3631, 35syl5 32 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( w  e.  ( U  i^i  ( B [,] C ) )  ->  w  <_  C
) )
3736ralrimiv 2876 . . . . . . . . . . . . 13  |-  ( ph  ->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  C )
38 breq2 4451 . . . . . . . . . . . . . . 15  |-  ( z  =  C  ->  (
w  <_  z  <->  w  <_  C ) )
3938ralbidv 2903 . . . . . . . . . . . . . 14  |-  ( z  =  C  ->  ( A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z  <->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  C )
)
4039rspcev 3214 . . . . . . . . . . . . 13  |-  ( ( C  e.  RR  /\  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  C )  ->  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )
4123, 37, 40syl2anc 661 . . . . . . . . . . . 12  |-  ( ph  ->  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )
42 suprcl 10499 . . . . . . . . . . . 12  |-  ( ( ( U  i^i  ( B [,] C ) ) 
C_  RR  /\  ( U  i^i  ( B [,] C ) )  =/=  (/)  /\  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )  ->  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )  e.  RR )
4318, 30, 41, 42syl3anc 1228 . . . . . . . . . . 11  |-  ( ph  ->  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )  e.  RR )
441, 43syl5eqel 2559 . . . . . . . . . 10  |-  ( ph  ->  S  e.  RR )
45 rphalfcl 11240 . . . . . . . . . 10  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
46 ltaddrp 11248 . . . . . . . . . 10  |-  ( ( S  e.  RR  /\  ( r  /  2
)  e.  RR+ )  ->  S  <  ( S  +  ( r  / 
2 ) ) )
4744, 45, 46syl2an 477 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  S  <  ( S  +  ( r  /  2 ) ) )
4844adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  S  e.  RR )
4945rpred 11252 . . . . . . . . . . 11  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR )
50 readdcl 9571 . . . . . . . . . . 11  |-  ( ( S  e.  RR  /\  ( r  /  2
)  e.  RR )  ->  ( S  +  ( r  /  2
) )  e.  RR )
5144, 49, 50syl2an 477 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S  +  ( r  / 
2 ) )  e.  RR )
5248, 51ltnled 9727 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S  <  ( S  +  ( r  /  2 ) )  <->  -.  ( S  +  ( r  / 
2 ) )  <_  S ) )
5347, 52mpbid 210 . . . . . . . 8  |-  ( (
ph  /\  r  e.  RR+ )  ->  -.  ( S  +  ( r  /  2 ) )  <_  S )
5418ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( U  i^i  ( B [,] C ) )  C_  RR )
5530ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( U  i^i  ( B [,] C ) )  =/=  (/) )
5641ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )
57 inss1 3718 . . . . . . . . . . . 12  |-  ( U  i^i  ( -oo (,) C ) )  C_  U
58 simpr 461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )
5957, 58sseldi 3502 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  U )
6051adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  RR )
6121ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  B  e.  RR )
6244ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  S  e.  RR )
63 suprub 10500 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( U  i^i  ( B [,] C ) )  C_  RR  /\  ( U  i^i  ( B [,] C ) )  =/=  (/)  /\  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )  /\  B  e.  ( U  i^i  ( B [,] C ) ) )  ->  B  <_  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  ) )
6418, 30, 41, 28, 63syl31anc 1231 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  <_  sup (
( U  i^i  ( B [,] C ) ) ,  RR ,  <  ) )
6564, 1syl6breqr 4487 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  <_  S )
6665ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  B  <_  S )
6747adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  S  <  ( S  +  ( r  /  2 ) ) )
6862, 60, 67ltled 9728 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  S  <_  ( S  +  ( r  /  2 ) ) )
6961, 62, 60, 66, 68letrd 9734 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  B  <_  ( S  +  ( r  /  2 ) ) )
7023ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  C  e.  RR )
71 inss2 3719 . . . . . . . . . . . . . . 15  |-  ( U  i^i  ( -oo (,) C ) )  C_  ( -oo (,) C )
7271, 58sseldi 3502 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  ( -oo (,) C ) )
73 eliooord 11580 . . . . . . . . . . . . . . 15  |-  ( ( S  +  ( r  /  2 ) )  e.  ( -oo (,) C )  ->  ( -oo  <  ( S  +  ( r  /  2
) )  /\  ( S  +  ( r  /  2 ) )  <  C ) )
7473simprd 463 . . . . . . . . . . . . . 14  |-  ( ( S  +  ( r  /  2 ) )  e.  ( -oo (,) C )  ->  ( S  +  ( r  /  2 ) )  <  C )
7572, 74syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  <  C )
7660, 70, 75ltled 9728 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  <_  C )
77 elicc2 11585 . . . . . . . . . . . . 13  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( ( S  +  ( r  /  2
) )  e.  ( B [,] C )  <-> 
( ( S  +  ( r  /  2
) )  e.  RR  /\  B  <_  ( S  +  ( r  / 
2 ) )  /\  ( S  +  (
r  /  2 ) )  <_  C )
) )
7861, 70, 77syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  (
( S  +  ( r  /  2 ) )  e.  ( B [,] C )  <->  ( ( S  +  ( r  /  2 ) )  e.  RR  /\  B  <_  ( S  +  ( r  /  2 ) )  /\  ( S  +  ( r  / 
2 ) )  <_  C ) ) )
7960, 69, 76, 78mpbir3and 1179 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  ( B [,] C ) )
8059, 79elind 3688 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( B [,] C ) ) )
81 suprub 10500 . . . . . . . . . 10  |-  ( ( ( ( U  i^i  ( B [,] C ) )  C_  RR  /\  ( U  i^i  ( B [,] C ) )  =/=  (/)  /\  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( B [,] C ) ) )  ->  ( S  +  ( r  /  2
) )  <_  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  ) )
8254, 55, 56, 80, 81syl31anc 1231 . . . . . . . . 9  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  <_  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )
)
8382, 1syl6breqr 4487 . . . . . . . 8  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  <_  S )
8453, 83mtand 659 . . . . . . 7  |-  ( (
ph  /\  r  e.  RR+ )  ->  -.  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )
85 eqid 2467 . . . . . . . . . . . . 13  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
8685remetdval 21029 . . . . . . . . . . . 12  |-  ( ( ( S  +  ( r  /  2 ) )  e.  RR  /\  S  e.  RR )  ->  ( ( S  +  ( r  /  2
) ) ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) S )  =  ( abs `  (
( S  +  ( r  /  2 ) )  -  S ) ) )
8751, 48, 86syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  +  ( r  /  2 ) ) ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) S )  =  ( abs `  ( ( S  +  ( r  /  2 ) )  -  S ) ) )
8848recnd 9618 . . . . . . . . . . . . 13  |-  ( (
ph  /\  r  e.  RR+ )  ->  S  e.  CC )
8949adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( r  /  2 )  e.  RR )
9089recnd 9618 . . . . . . . . . . . . 13  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( r  /  2 )  e.  CC )
9188, 90pncan2d 9928 . . . . . . . . . . . 12  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  +  ( r  /  2 ) )  -  S )  =  ( r  /  2
) )
9291fveq2d 5868 . . . . . . . . . . 11  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( abs `  ( ( S  +  ( r  /  2
) )  -  S
) )  =  ( abs `  ( r  /  2 ) ) )
9345adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( r  /  2 )  e.  RR+ )
94 rpre 11222 . . . . . . . . . . . . 13  |-  ( ( r  /  2 )  e.  RR+  ->  ( r  /  2 )  e.  RR )
95 rpge0 11228 . . . . . . . . . . . . 13  |-  ( ( r  /  2 )  e.  RR+  ->  0  <_ 
( r  /  2
) )
9694, 95absidd 13213 . . . . . . . . . . . 12  |-  ( ( r  /  2 )  e.  RR+  ->  ( abs `  ( r  /  2
) )  =  ( r  /  2 ) )
9793, 96syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( abs `  ( r  /  2
) )  =  ( r  /  2 ) )
9887, 92, 973eqtrd 2512 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  +  ( r  /  2 ) ) ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) S )  =  ( r  /  2 ) )
99 rphalflt 11242 . . . . . . . . . . 11  |-  ( r  e.  RR+  ->  ( r  /  2 )  < 
r )
10099adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( r  /  2 )  < 
r )
10198, 100eqbrtrd 4467 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  +  ( r  /  2 ) ) ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) S )  <  r
)
10285rexmet 21031 . . . . . . . . . . 11  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  e.  ( *Met `  RR )
103102a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  e.  ( *Met `  RR ) )
104 rpxr 11223 . . . . . . . . . . 11  |-  ( r  e.  RR+  ->  r  e. 
RR* )
105104adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  r  e.  RR* )
106 elbl3 20630 . . . . . . . . . 10  |-  ( ( ( ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) )  e.  ( *Met `  RR )  /\  r  e.  RR* )  /\  ( S  e.  RR  /\  ( S  +  ( r  /  2 ) )  e.  RR ) )  ->  ( ( S  +  ( r  / 
2 ) )  e.  ( S ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  <->  ( ( S  +  ( r  /  2 ) ) ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) S )  <  r
) )
107103, 105, 48, 51, 106syl22anc 1229 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  +  ( r  /  2 ) )  e.  ( S (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  <->  ( ( S  +  ( r  / 
2 ) ) ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) S )  <  r ) )
108101, 107mpbird 232 . . . . . . . 8  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S  +  ( r  / 
2 ) )  e.  ( S ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r ) )
109 ssel 3498 . . . . . . . 8  |-  ( ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C
) )  ->  (
( S  +  ( r  /  2 ) )  e.  ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  ->  ( S  +  ( r  / 
2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) ) )
110108, 109syl5com 30 . . . . . . 7  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C
) )  ->  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) ) )
11184, 110mtod 177 . . . . . 6  |-  ( (
ph  /\  r  e.  RR+ )  ->  -.  ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C
) ) )
112111nrexdv 2920 . . . . 5  |-  ( ph  ->  -.  E. r  e.  RR+  ( S ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C ) ) )
11344adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  S  e.  U )  ->  S  e.  RR )
114 mnflt 11329 . . . . . . . . . 10  |-  ( S  e.  RR  -> -oo  <  S )
115113, 114syl 16 . . . . . . . . 9  |-  ( (
ph  /\  S  e.  U )  -> -oo  <  S )
116 suprleub 10503 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( U  i^i  ( B [,] C ) )  C_  RR  /\  ( U  i^i  ( B [,] C ) )  =/=  (/)  /\  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )  /\  C  e.  RR )  ->  ( sup (
( U  i^i  ( B [,] C ) ) ,  RR ,  <  )  <_  C  <->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  C )
)
11718, 30, 41, 23, 116syl31anc 1231 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )  <_  C  <->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  C )
)
11837, 117mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ph  ->  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )  <_  C )
1191, 118syl5eqbr 4480 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  <_  C )
12044, 23leloed 9723 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( S  <_  C  <->  ( S  <  C  \/  S  =  C )
) )
121119, 120mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  <  C  \/  S  =  C
) )
122121ord 377 . . . . . . . . . . . 12  |-  ( ph  ->  ( -.  S  < 
C  ->  S  =  C ) )
123 elndif 3628 . . . . . . . . . . . . . . 15  |-  ( C  e.  A  ->  -.  C  e.  ( RR  \  A ) )
1248, 123syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  -.  C  e.  ( RR  \  A ) )
125 inss1 3718 . . . . . . . . . . . . . . . 16  |-  ( V  i^i  A )  C_  V
126125, 7sseldi 3502 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  V )
127 elin 3687 . . . . . . . . . . . . . . . 16  |-  ( C  e.  ( U  i^i  V )  <->  ( C  e.  U  /\  C  e.  V ) )
128 reconnlem2.7 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( U  i^i  V
)  C_  ( RR  \  A ) )
129128sseld 3503 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( C  e.  ( U  i^i  V )  ->  C  e.  ( RR  \  A ) ) )
130127, 129syl5bir 218 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( C  e.  U  /\  C  e.  V )  ->  C  e.  ( RR  \  A
) ) )
131126, 130mpan2d 674 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( C  e.  U  ->  C  e.  ( RR 
\  A ) ) )
132124, 131mtod 177 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  C  e.  U
)
133 eleq1 2539 . . . . . . . . . . . . . 14  |-  ( S  =  C  ->  ( S  e.  U  <->  C  e.  U ) )
134133notbid 294 . . . . . . . . . . . . 13  |-  ( S  =  C  ->  ( -.  S  e.  U  <->  -.  C  e.  U ) )
135132, 134syl5ibrcom 222 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  =  C  ->  -.  S  e.  U ) )
136122, 135syld 44 . . . . . . . . . . 11  |-  ( ph  ->  ( -.  S  < 
C  ->  -.  S  e.  U ) )
137136con4d 105 . . . . . . . . . 10  |-  ( ph  ->  ( S  e.  U  ->  S  <  C ) )
138137imp 429 . . . . . . . . 9  |-  ( (
ph  /\  S  e.  U )  ->  S  <  C )
139 mnfxr 11319 . . . . . . . . . . 11  |- -oo  e.  RR*
140 elioo2 11566 . . . . . . . . . . 11  |-  ( ( -oo  e.  RR*  /\  C  e.  RR* )  ->  ( S  e.  ( -oo (,) C )  <->  ( S  e.  RR  /\ -oo  <  S  /\  S  <  C
) ) )
141139, 24, 140sylancr 663 . . . . . . . . . 10  |-  ( ph  ->  ( S  e.  ( -oo (,) C )  <-> 
( S  e.  RR  /\ -oo  <  S  /\  S  <  C ) ) )
142141adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  S  e.  U )  ->  ( S  e.  ( -oo (,) C )  <->  ( S  e.  RR  /\ -oo  <  S  /\  S  <  C
) ) )
143113, 115, 138, 142mpbir3and 1179 . . . . . . . 8  |-  ( (
ph  /\  S  e.  U )  ->  S  e.  ( -oo (,) C
) )
144143ex 434 . . . . . . 7  |-  ( ph  ->  ( S  e.  U  ->  S  e.  ( -oo (,) C ) ) )
145144ancld 553 . . . . . 6  |-  ( ph  ->  ( S  e.  U  ->  ( S  e.  U  /\  S  e.  ( -oo (,) C ) ) ) )
146 elin 3687 . . . . . . 7  |-  ( S  e.  ( U  i^i  ( -oo (,) C ) )  <->  ( S  e.  U  /\  S  e.  ( -oo (,) C
) ) )
147 reconnlem2.2 . . . . . . . 8  |-  ( ph  ->  U  e.  ( topGen ` 
ran  (,) ) )
148 retop 21003 . . . . . . . . 9  |-  ( topGen ` 
ran  (,) )  e.  Top
149 iooretop 21008 . . . . . . . . 9  |-  ( -oo (,) C )  e.  (
topGen `  ran  (,) )
150 inopn 19175 . . . . . . . . 9  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  U  e.  ( topGen `  ran  (,) )  /\  ( -oo (,) C
)  e.  ( topGen ` 
ran  (,) ) )  -> 
( U  i^i  ( -oo (,) C ) )  e.  ( topGen `  ran  (,) ) )
151148, 149, 150mp3an13 1315 . . . . . . . 8  |-  ( U  e.  ( topGen `  ran  (,) )  ->  ( U  i^i  ( -oo (,) C
) )  e.  (
topGen `  ran  (,) )
)
152 eqid 2467 . . . . . . . . . . . 12  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
15385, 152tgioo 21036 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
154153mopni2 20731 . . . . . . . . . 10  |-  ( ( ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )  e.  ( *Met `  RR )  /\  ( U  i^i  ( -oo (,) C ) )  e.  ( topGen `  ran  (,) )  /\  S  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  E. r  e.  RR+  ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C
) ) )
155102, 154mp3an1 1311 . . . . . . . . 9  |-  ( ( ( U  i^i  ( -oo (,) C ) )  e.  ( topGen `  ran  (,) )  /\  S  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  E. r  e.  RR+  ( S (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C
) ) )
156155ex 434 . . . . . . . 8  |-  ( ( U  i^i  ( -oo (,) C ) )  e.  ( topGen `  ran  (,) )  ->  ( S  e.  ( U  i^i  ( -oo (,) C ) )  ->  E. r  e.  RR+  ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C
) ) ) )
157147, 151, 1563syl 20 . . . . . . 7  |-  ( ph  ->  ( S  e.  ( U  i^i  ( -oo (,) C ) )  ->  E. r  e.  RR+  ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C
) ) ) )
158146, 157syl5bir 218 . . . . . 6  |-  ( ph  ->  ( ( S  e.  U  /\  S  e.  ( -oo (,) C
) )  ->  E. r  e.  RR+  ( S (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C
) ) ) )
159145, 158syld 44 . . . . 5  |-  ( ph  ->  ( S  e.  U  ->  E. r  e.  RR+  ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C
) ) ) )
160112, 159mtod 177 . . . 4  |-  ( ph  ->  -.  S  e.  U
)
161 ltsubrp 11247 . . . . . . . . 9  |-  ( ( S  e.  RR  /\  r  e.  RR+ )  -> 
( S  -  r
)  <  S )
16244, 161sylan 471 . . . . . . . 8  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S  -  r )  < 
S )
163 rpre 11222 . . . . . . . . . 10  |-  ( r  e.  RR+  ->  r  e.  RR )
164 resubcl 9879 . . . . . . . . . 10  |-  ( ( S  e.  RR  /\  r  e.  RR )  ->  ( S  -  r
)  e.  RR )
16544, 163, 164syl2an 477 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S  -  r )  e.  RR )
166165, 48ltnled 9727 . . . . . . . 8  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  -  r )  <  S  <->  -.  S  <_  ( S  -  r ) ) )
167162, 166mpbid 210 . . . . . . 7  |-  ( (
ph  /\  r  e.  RR+ )  ->  -.  S  <_  ( S  -  r
) )
16885bl2ioo 21032 . . . . . . . . . 10  |-  ( ( S  e.  RR  /\  r  e.  RR )  ->  ( S ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  =  ( ( S  -  r ) (,) ( S  +  r )
) )
16944, 163, 168syl2an 477 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  =  ( ( S  -  r ) (,) ( S  +  r ) ) )
170169sseq1d 3531 . . . . . . . 8  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V  <->  ( ( S  -  r ) (,) ( S  +  r ) )  C_  V
) )
17115ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( B [,] C
)  C_  A )
1722, 171syl5ss 3515 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( U  i^i  ( B [,] C ) ) 
C_  A )
173172sselda 3504 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  w  e.  A
)
174 elndif 3628 . . . . . . . . . . . . . . 15  |-  ( w  e.  A  ->  -.  w  e.  ( RR  \  A ) )
175173, 174syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  -.  w  e.  ( RR  \  A ) )
176128ad3antrrr 729 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  ( U  i^i  V )  C_  ( RR  \  A ) )
177 inss1 3718 . . . . . . . . . . . . . . . . . 18  |-  ( U  i^i  ( B [,] C ) )  C_  U
178 simprl 755 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  e.  ( U  i^i  ( B [,] C ) ) )
179177, 178sseldi 3502 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  e.  U )
180 simplr 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )
18118ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  ( U  i^i  ( B [,] C ) )  C_  RR )
182 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  w  e.  ( U  i^i  ( B [,] C ) ) )
183181, 182sseldd 3505 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  w  e.  RR )
184183adantrr 716 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  e.  RR )
185 simprr 756 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  ( S  -  r )  <  w )
18648ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  S  e.  RR )
187 simpllr 758 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  r  e.  RR+ )
188187rpred 11252 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  r  e.  RR )
189186, 188readdcld 9619 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  ( S  +  r )  e.  RR )
190181adantrr 716 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  ( U  i^i  ( B [,] C ) )  C_  RR )
19130ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  ( U  i^i  ( B [,] C ) )  =/=  (/) )
19241ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )
193 suprub 10500 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( U  i^i  ( B [,] C ) )  C_  RR  /\  ( U  i^i  ( B [,] C ) )  =/=  (/)  /\  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  w  <_  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  ) )
194190, 191, 192, 178, 193syl31anc 1231 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  <_  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )
)
195194, 1syl6breqr 4487 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  <_  S )
196186, 187ltaddrpd 11281 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  S  <  ( S  +  r ) )
197184, 186, 189, 195, 196lelttrd 9735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  <  ( S  +  r ) )
198165ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  ( S  -  r )  e.  RR )
199 rexr 9635 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  -  r )  e.  RR  ->  ( S  -  r )  e.  RR* )
200 rexr 9635 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  +  r )  e.  RR  ->  ( S  +  r )  e.  RR* )
201 elioo2 11566 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( S  -  r
)  e.  RR*  /\  ( S  +  r )  e.  RR* )  ->  (
w  e.  ( ( S  -  r ) (,) ( S  +  r ) )  <->  ( w  e.  RR  /\  ( S  -  r )  < 
w  /\  w  <  ( S  +  r ) ) ) )
202199, 200, 201syl2an 477 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( S  -  r
)  e.  RR  /\  ( S  +  r
)  e.  RR )  ->  ( w  e.  ( ( S  -  r ) (,) ( S  +  r )
)  <->  ( w  e.  RR  /\  ( S  -  r )  < 
w  /\  w  <  ( S  +  r ) ) ) )
203198, 189, 202syl2anc 661 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  (
w  e.  ( ( S  -  r ) (,) ( S  +  r ) )  <->  ( w  e.  RR  /\  ( S  -  r )  < 
w  /\  w  <  ( S  +  r ) ) ) )
204184, 185, 197, 203mpbir3and 1179 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  e.  ( ( S  -  r ) (,) ( S  +  r )
) )
205180, 204sseldd 3505 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  e.  V )
206179, 205elind 3688 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  e.  ( U  i^i  V
) )
207176, 206sseldd 3505 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  ( w  e.  ( U  i^i  ( B [,] C ) )  /\  ( S  -  r )  <  w
) )  ->  w  e.  ( RR  \  A
) )
208207expr 615 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  ( ( S  -  r )  < 
w  ->  w  e.  ( RR  \  A ) ) )
209175, 208mtod 177 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  -.  ( S  -  r )  < 
w )
210165ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  ( S  -  r )  e.  RR )
211183, 210lenltd 9726 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  ( w  <_ 
( S  -  r
)  <->  -.  ( S  -  r )  < 
w ) )
212209, 211mpbird 232 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  w  <_  ( S  -  r )
)
213212ralrimiva 2878 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  ->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  ( S  -  r ) )
21418ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( U  i^i  ( B [,] C ) ) 
C_  RR )
21530ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( U  i^i  ( B [,] C ) )  =/=  (/) )
21641ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  ->  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )
217165adantr 465 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( S  -  r
)  e.  RR )
218 suprleub 10503 . . . . . . . . . . . 12  |-  ( ( ( ( U  i^i  ( B [,] C ) )  C_  RR  /\  ( U  i^i  ( B [,] C ) )  =/=  (/)  /\  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )  /\  ( S  -  r
)  e.  RR )  ->  ( sup (
( U  i^i  ( B [,] C ) ) ,  RR ,  <  )  <_  ( S  -  r )  <->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  ( S  -  r ) ) )
219214, 215, 216, 217, 218syl31anc 1231 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )  <_  ( S  -  r )  <->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  ( S  -  r ) ) )
220213, 219mpbird 232 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  ->  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )  <_  ( S  -  r ) )
2211, 220syl5eqbr 4480 . . . . . . . . 9  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  ->  S  <_  ( S  -  r ) )
222221ex 434 . . . . . . . 8  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V  ->  S  <_  ( S  -  r
) ) )
223170, 222sylbid 215 . . . . . . 7  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V  ->  S  <_  ( S  -  r ) ) )
224167, 223mtod 177 . . . . . 6  |-  ( (
ph  /\  r  e.  RR+ )  ->  -.  ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V )
225224nrexdv 2920 . . . . 5  |-  ( ph  ->  -.  E. r  e.  RR+  ( S ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  C_  V )
226 reconnlem2.3 . . . . . 6  |-  ( ph  ->  V  e.  ( topGen ` 
ran  (,) ) )
227153mopni2 20731 . . . . . . . 8  |-  ( ( ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )  e.  ( *Met `  RR )  /\  V  e.  ( topGen `  ran  (,) )  /\  S  e.  V
)  ->  E. r  e.  RR+  ( S (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V )
228102, 227mp3an1 1311 . . . . . . 7  |-  ( ( V  e.  ( topGen ` 
ran  (,) )  /\  S  e.  V )  ->  E. r  e.  RR+  ( S (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V )
229228ex 434 . . . . . 6  |-  ( V  e.  ( topGen `  ran  (,) )  ->  ( S  e.  V  ->  E. r  e.  RR+  ( S (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V )
)
230226, 229syl 16 . . . . 5  |-  ( ph  ->  ( S  e.  V  ->  E. r  e.  RR+  ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V )
)
231225, 230mtod 177 . . . 4  |-  ( ph  ->  -.  S  e.  V
)
232 ioran 490 . . . 4  |-  ( -.  ( S  e.  U  \/  S  e.  V
)  <->  ( -.  S  e.  U  /\  -.  S  e.  V ) )
233160, 231, 232sylanbrc 664 . . 3  |-  ( ph  ->  -.  ( S  e.  U  \/  S  e.  V ) )
234 elun 3645 . . 3  |-  ( S  e.  ( U  u.  V )  <->  ( S  e.  U  \/  S  e.  V ) )
235233, 234sylnibr 305 . 2  |-  ( ph  ->  -.  S  e.  ( U  u.  V ) )
236 elicc2 11585 . . . . . 6  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( S  e.  ( B [,] C )  <-> 
( S  e.  RR  /\  B  <_  S  /\  S  <_  C ) ) )
23721, 23, 236syl2anc 661 . . . . 5  |-  ( ph  ->  ( S  e.  ( B [,] C )  <-> 
( S  e.  RR  /\  B  <_  S  /\  S  <_  C ) ) )
23844, 65, 119, 237mpbir3and 1179 . . . 4  |-  ( ph  ->  S  e.  ( B [,] C ) )
23915, 238sseldd 3505 . . 3  |-  ( ph  ->  S  e.  A )
240 ssel 3498 . . 3  |-  ( A 
C_  ( U  u.  V )  ->  ( S  e.  A  ->  S  e.  ( U  u.  V ) ) )
241239, 240syl5com 30 . 2  |-  ( ph  ->  ( A  C_  ( U  u.  V )  ->  S  e.  ( U  u.  V ) ) )
242235, 241mtod 177 1  |-  ( ph  ->  -.  A  C_  ( U  u.  V )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767    =/= wne 2662   A.wral 2814   E.wrex 2815    \ cdif 3473    u. cun 3474    i^i cin 3475    C_ wss 3476   (/)c0 3785   class class class wbr 4447    X. cxp 4997   ran crn 5000    |` cres 5001    o. ccom 5003   ` cfv 5586  (class class class)co 6282   supcsup 7896   RRcr 9487    + caddc 9491   -oocmnf 9622   RR*cxr 9623    < clt 9624    <_ cle 9625    - cmin 9801    / cdiv 10202   2c2 10581   RR+crp 11216   (,)cioo 11525   [,]cicc 11528   abscabs 13026   topGenctg 14689   *Metcxmt 18174   ballcbl 18176   MetOpencmopn 18179   Topctop 19161
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565  ax-pre-sup 9566
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-er 7308  df-map 7419  df-en 7514  df-dom 7515  df-sdom 7516  df-sup 7897  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-div 10203  df-nn 10533  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11079  df-q 11179  df-rp 11217  df-xneg 11314  df-xadd 11315  df-xmul 11316  df-ioo 11529  df-icc 11532  df-seq 12072  df-exp 12131  df-cj 12891  df-re 12892  df-im 12893  df-sqrt 13027  df-abs 13028  df-topgen 14695  df-psmet 18182  df-xmet 18183  df-met 18184  df-bl 18185  df-mopn 18186  df-top 19166  df-bases 19168  df-topon 19169
This theorem is referenced by:  reconn  21068
  Copyright terms: Public domain W3C validator