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

Theorem reconnlem2 21624
Description: Lemma for reconn 21625. (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 3660 . . . . . . . . . . . . 13  |-  ( U  i^i  ( B [,] C ) )  C_  ( B [,] C )
3 inss2 3660 . . . . . . . . . . . . . . . 16  |-  ( U  i^i  A )  C_  A
4 reconnlem2.5 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  B  e.  ( U  i^i  A ) )
53, 4sseldi 3440 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  A )
6 inss2 3660 . . . . . . . . . . . . . . . 16  |-  ( V  i^i  A )  C_  A
7 reconnlem2.6 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  ( V  i^i  A ) )
86, 7sseldi 3440 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  A )
9 reconnlem2.4 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. x  e.  A  A. y  e.  A  ( x [,] y
)  C_  A )
10 oveq1 6285 . . . . . . . . . . . . . . . . 17  |-  ( x  =  B  ->  (
x [,] y )  =  ( B [,] y ) )
1110sseq1d 3469 . . . . . . . . . . . . . . . 16  |-  ( x  =  B  ->  (
( x [,] y
)  C_  A  <->  ( B [,] y )  C_  A
) )
12 oveq2 6286 . . . . . . . . . . . . . . . . 17  |-  ( y  =  C  ->  ( B [,] y )  =  ( B [,] C
) )
1312sseq1d 3469 . . . . . . . . . . . . . . . 16  |-  ( y  =  C  ->  (
( B [,] y
)  C_  A  <->  ( B [,] C )  C_  A
) )
1411, 13rspc2va 3170 . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B [,] C
)  C_  A )
16 reconnlem2.1 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  RR )
1715, 16sstrd 3452 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B [,] C
)  C_  RR )
182, 17syl5ss 3453 . . . . . . . . . . . 12  |-  ( ph  ->  ( U  i^i  ( B [,] C ) ) 
C_  RR )
19 inss1 3659 . . . . . . . . . . . . . . 15  |-  ( U  i^i  A )  C_  U
2019, 4sseldi 3440 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  U )
2116, 5sseldd 3443 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  B  e.  RR )
2221rexrd 9673 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  RR* )
2316, 8sseldd 3443 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  e.  RR )
2423rexrd 9673 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  RR* )
25 reconnlem2.8 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  <_  C )
26 lbicc2 11690 . . . . . . . . . . . . . . 15  |-  ( ( B  e.  RR*  /\  C  e.  RR*  /\  B  <_  C )  ->  B  e.  ( B [,] C
) )
2722, 24, 25, 26syl3anc 1230 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  ( B [,] C ) )
2820, 27elind 3627 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  ( U  i^i  ( B [,] C ) ) )
29 ne0i 3744 . . . . . . . . . . . . 13  |-  ( B  e.  ( U  i^i  ( B [,] C ) )  ->  ( U  i^i  ( B [,] C
) )  =/=  (/) )
3028, 29syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( U  i^i  ( B [,] C ) )  =/=  (/) )
312sseli 3438 . . . . . . . . . . . . . . 15  |-  ( w  e.  ( U  i^i  ( B [,] C ) )  ->  w  e.  ( B [,] C ) )
32 elicc2 11643 . . . . . . . . . . . . . . . . 17  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( w  e.  ( B [,] C )  <-> 
( w  e.  RR  /\  B  <_  w  /\  w  <_  C ) ) )
3321, 23, 32syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( w  e.  ( B [,] C )  <-> 
( w  e.  RR  /\  B  <_  w  /\  w  <_  C ) ) )
34 simp3 999 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  RR  /\  B  <_  w  /\  w  <_  C )  ->  w  <_  C )
3533, 34syl6bi 228 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( w  e.  ( B [,] C )  ->  w  <_  C
) )
3631, 35syl5 30 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( w  e.  ( U  i^i  ( B [,] C ) )  ->  w  <_  C
) )
3736ralrimiv 2816 . . . . . . . . . . . . 13  |-  ( ph  ->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  C )
38 breq2 4399 . . . . . . . . . . . . . . 15  |-  ( z  =  C  ->  (
w  <_  z  <->  w  <_  C ) )
3938ralbidv 2843 . . . . . . . . . . . . . 14  |-  ( z  =  C  ->  ( A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z  <->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  C )
)
4039rspcev 3160 . . . . . . . . . . . . 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 659 . . . . . . . . . . . 12  |-  ( ph  ->  E. z  e.  RR  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  z )
42 suprcl 10543 . . . . . . . . . . . 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 1230 . . . . . . . . . . 11  |-  ( ph  ->  sup ( ( U  i^i  ( B [,] C ) ) ,  RR ,  <  )  e.  RR )
441, 43syl5eqel 2494 . . . . . . . . . 10  |-  ( ph  ->  S  e.  RR )
45 rphalfcl 11290 . . . . . . . . . 10  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR+ )
46 ltaddrp 11299 . . . . . . . . . 10  |-  ( ( S  e.  RR  /\  ( r  /  2
)  e.  RR+ )  ->  S  <  ( S  +  ( r  / 
2 ) ) )
4744, 45, 46syl2an 475 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  S  <  ( S  +  ( r  /  2 ) ) )
4844adantr 463 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  S  e.  RR )
4945rpred 11304 . . . . . . . . . . 11  |-  ( r  e.  RR+  ->  ( r  /  2 )  e.  RR )
50 readdcl 9605 . . . . . . . . . . 11  |-  ( ( S  e.  RR  /\  ( r  /  2
)  e.  RR )  ->  ( S  +  ( r  /  2
) )  e.  RR )
5144, 49, 50syl2an 475 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S  +  ( r  / 
2 ) )  e.  RR )
5248, 51ltnled 9764 . . . . . . . . 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 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( U  i^i  ( B [,] C ) )  C_  RR )
5530ad2antrr 724 . . . . . . . . . 10  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( U  i^i  ( B [,] C ) )  =/=  (/) )
5641ad2antrr 724 . . . . . . . . . 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 3659 . . . . . . . . . . . 12  |-  ( U  i^i  ( -oo (,) C ) )  C_  U
58 simpr 459 . . . . . . . . . . . 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 3440 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  U )
6051adantr 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  RR )
6121ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  B  e.  RR )
6244ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  S  e.  RR )
63 suprub 10544 . . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  <_  sup (
( U  i^i  ( B [,] C ) ) ,  RR ,  <  ) )
6564, 1syl6breqr 4435 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  <_  S )
6665ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  B  <_  S )
6747adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  S  <  ( S  +  ( r  /  2 ) ) )
6862, 60, 67ltled 9765 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  S  <_  ( S  +  ( r  /  2 ) ) )
6961, 62, 60, 66, 68letrd 9773 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  B  <_  ( S  +  ( r  /  2 ) ) )
7023ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  C  e.  RR )
71 inss2 3660 . . . . . . . . . . . . . . 15  |-  ( U  i^i  ( -oo (,) C ) )  C_  ( -oo (,) C )
7271, 58sseldi 3440 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  ( -oo (,) C ) )
73 eliooord 11638 . . . . . . . . . . . . . . 15  |-  ( ( S  +  ( r  /  2 ) )  e.  ( -oo (,) C )  ->  ( -oo  <  ( S  +  ( r  /  2
) )  /\  ( S  +  ( r  /  2 ) )  <  C ) )
7473simprd 461 . . . . . . . . . . . . . 14  |-  ( ( S  +  ( r  /  2 ) )  e.  ( -oo (,) C )  ->  ( S  +  ( r  /  2 ) )  <  C )
7572, 74syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  <  C )
7660, 70, 75ltled 9765 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  <_  C )
77 elicc2 11643 . . . . . . . . . . . . 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 659 . . . . . . . . . . . 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 1180 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  e.  ( B [,] C ) )
8059, 79elind 3627 . . . . . . . . . 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 10544 . . . . . . . . . 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 1233 . . . . . . . . 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 4435 . . . . . . . 8  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )  ->  ( S  +  ( r  /  2 ) )  <_  S )
8453, 83mtand 657 . . . . . . 7  |-  ( (
ph  /\  r  e.  RR+ )  ->  -.  ( S  +  ( r  /  2 ) )  e.  ( U  i^i  ( -oo (,) C ) ) )
85 eqid 2402 . . . . . . . . . . . . 13  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
8685remetdval 21586 . . . . . . . . . . . 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 659 . . . . . . . . . . 11  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  +  ( r  /  2 ) ) ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) S )  =  ( abs `  ( ( S  +  ( r  /  2 ) )  -  S ) ) )
8848recnd 9652 . . . . . . . . . . . . 13  |-  ( (
ph  /\  r  e.  RR+ )  ->  S  e.  CC )
8949adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( r  /  2 )  e.  RR )
9089recnd 9652 . . . . . . . . . . . . 13  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( r  /  2 )  e.  CC )
9188, 90pncan2d 9969 . . . . . . . . . . . 12  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  +  ( r  /  2 ) )  -  S )  =  ( r  /  2
) )
9291fveq2d 5853 . . . . . . . . . . 11  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( abs `  ( ( S  +  ( r  /  2
) )  -  S
) )  =  ( abs `  ( r  /  2 ) ) )
9345adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( r  /  2 )  e.  RR+ )
94 rpre 11271 . . . . . . . . . . . . 13  |-  ( ( r  /  2 )  e.  RR+  ->  ( r  /  2 )  e.  RR )
95 rpge0 11277 . . . . . . . . . . . . 13  |-  ( ( r  /  2 )  e.  RR+  ->  0  <_ 
( r  /  2
) )
9694, 95absidd 13403 . . . . . . . . . . . 12  |-  ( ( r  /  2 )  e.  RR+  ->  ( abs `  ( r  /  2
) )  =  ( r  /  2 ) )
9793, 96syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( abs `  ( r  /  2
) )  =  ( r  /  2 ) )
9887, 92, 973eqtrd 2447 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  +  ( r  /  2 ) ) ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) S )  =  ( r  /  2 ) )
99 rphalflt 11292 . . . . . . . . . . 11  |-  ( r  e.  RR+  ->  ( r  /  2 )  < 
r )
10099adantl 464 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( r  /  2 )  < 
r )
10198, 100eqbrtrd 4415 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  +  ( r  /  2 ) ) ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) S )  <  r
)
10285rexmet 21588 . . . . . . . . . . 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 11272 . . . . . . . . . . 11  |-  ( r  e.  RR+  ->  r  e. 
RR* )
105104adantl 464 . . . . . . . . . 10  |-  ( (
ph  /\  r  e.  RR+ )  ->  r  e.  RR* )
106 elbl3 21187 . . . . . . . . . 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 1231 . . . . . . . . 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 3436 . . . . . . . 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 28 . . . . . . 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 2860 . . . . 5  |-  ( ph  ->  -.  E. r  e.  RR+  ( S ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  C_  ( U  i^i  ( -oo (,) C ) ) )
11344adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  S  e.  U )  ->  S  e.  RR )
114 mnflt 11386 . . . . . . . . . 10  |-  ( S  e.  RR  -> -oo  <  S )
115113, 114syl 17 . . . . . . . . 9  |-  ( (
ph  /\  S  e.  U )  -> -oo  <  S )
116 suprleub 10547 . . . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . . . 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 4428 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  <_  C )
12044, 23leloed 9760 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( S  <_  C  <->  ( S  <  C  \/  S  =  C )
) )
121119, 120mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  <  C  \/  S  =  C
) )
122121ord 375 . . . . . . . . . . . 12  |-  ( ph  ->  ( -.  S  < 
C  ->  S  =  C ) )
123 elndif 3567 . . . . . . . . . . . . . . 15  |-  ( C  e.  A  ->  -.  C  e.  ( RR  \  A ) )
1248, 123syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  -.  C  e.  ( RR  \  A ) )
125 inss1 3659 . . . . . . . . . . . . . . . 16  |-  ( V  i^i  A )  C_  V
126125, 7sseldi 3440 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  e.  V )
127 elin 3626 . . . . . . . . . . . . . . . 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 3441 . . . . . . . . . . . . . . . 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 672 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( C  e.  U  ->  C  e.  ( RR 
\  A ) ) )
132124, 131mtod 177 . . . . . . . . . . . . 13  |-  ( ph  ->  -.  C  e.  U
)
133 eleq1 2474 . . . . . . . . . . . . . 14  |-  ( S  =  C  ->  ( S  e.  U  <->  C  e.  U ) )
134133notbid 292 . . . . . . . . . . . . 13  |-  ( S  =  C  ->  ( -.  S  e.  U  <->  -.  C  e.  U ) )
135132, 134syl5ibrcom 222 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  =  C  ->  -.  S  e.  U ) )
136122, 135syld 42 . . . . . . . . . . 11  |-  ( ph  ->  ( -.  S  < 
C  ->  -.  S  e.  U ) )
137136con4d 105 . . . . . . . . . 10  |-  ( ph  ->  ( S  e.  U  ->  S  <  C ) )
138137imp 427 . . . . . . . . 9  |-  ( (
ph  /\  S  e.  U )  ->  S  <  C )
139 mnfxr 11376 . . . . . . . . . . 11  |- -oo  e.  RR*
140 elioo2 11623 . . . . . . . . . . 11  |-  ( ( -oo  e.  RR*  /\  C  e.  RR* )  ->  ( S  e.  ( -oo (,) C )  <->  ( S  e.  RR  /\ -oo  <  S  /\  S  <  C
) ) )
141139, 24, 140sylancr 661 . . . . . . . . . 10  |-  ( ph  ->  ( S  e.  ( -oo (,) C )  <-> 
( S  e.  RR  /\ -oo  <  S  /\  S  <  C ) ) )
142141adantr 463 . . . . . . . . 9  |-  ( (
ph  /\  S  e.  U )  ->  ( S  e.  ( -oo (,) C )  <->  ( S  e.  RR  /\ -oo  <  S  /\  S  <  C
) ) )
143113, 115, 138, 142mpbir3and 1180 . . . . . . . 8  |-  ( (
ph  /\  S  e.  U )  ->  S  e.  ( -oo (,) C
) )
144143ex 432 . . . . . . 7  |-  ( ph  ->  ( S  e.  U  ->  S  e.  ( -oo (,) C ) ) )
145144ancld 551 . . . . . 6  |-  ( ph  ->  ( S  e.  U  ->  ( S  e.  U  /\  S  e.  ( -oo (,) C ) ) ) )
146 elin 3626 . . . . . . 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 21560 . . . . . . . . 9  |-  ( topGen ` 
ran  (,) )  e.  Top
149 iooretop 21565 . . . . . . . . 9  |-  ( -oo (,) C )  e.  (
topGen `  ran  (,) )
150 inopn 19700 . . . . . . . . 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 1317 . . . . . . . 8  |-  ( U  e.  ( topGen `  ran  (,) )  ->  ( U  i^i  ( -oo (,) C
) )  e.  (
topGen `  ran  (,) )
)
152 eqid 2402 . . . . . . . . . . . 12  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
15385, 152tgioo 21593 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
154153mopni2 21288 . . . . . . . . . 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 1313 . . . . . . . . 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 432 . . . . . . . 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 18 . . . . . . 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 42 . . . . 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 11298 . . . . . . . . 9  |-  ( ( S  e.  RR  /\  r  e.  RR+ )  -> 
( S  -  r
)  <  S )
16244, 161sylan 469 . . . . . . . 8  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S  -  r )  < 
S )
163 rpre 11271 . . . . . . . . . 10  |-  ( r  e.  RR+  ->  r  e.  RR )
164 resubcl 9919 . . . . . . . . . 10  |-  ( ( S  e.  RR  /\  r  e.  RR )  ->  ( S  -  r
)  e.  RR )
16544, 163, 164syl2an 475 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S  -  r )  e.  RR )
166165, 48ltnled 9764 . . . . . . . 8  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S  -  r )  <  S  <->  -.  S  <_  ( S  -  r ) ) )
167162, 166mpbid 210 . . . . . . 7  |-  ( (
ph  /\  r  e.  RR+ )  ->  -.  S  <_  ( S  -  r
) )
16885bl2ioo 21589 . . . . . . . . . 10  |-  ( ( S  e.  RR  /\  r  e.  RR )  ->  ( S ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  =  ( ( S  -  r ) (,) ( S  +  r )
) )
16944, 163, 168syl2an 475 . . . . . . . . 9  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( S
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  =  ( ( S  -  r ) (,) ( S  +  r ) ) )
170169sseq1d 3469 . . . . . . . 8  |-  ( (
ph  /\  r  e.  RR+ )  ->  ( ( S ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V  <->  ( ( S  -  r ) (,) ( S  +  r ) )  C_  V
) )
17115ad2antrr 724 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( B [,] C
)  C_  A )
1722, 171syl5ss 3453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( U  i^i  ( B [,] C ) ) 
C_  A )
173172sselda 3442 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  w  e.  A
)
174 elndif 3567 . . . . . . . . . . . . . . 15  |-  ( w  e.  A  ->  -.  w  e.  ( RR  \  A ) )
175173, 174syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  -.  w  e.  ( RR  \  A ) )
176128ad3antrrr 728 . . . . . . . . . . . . . . . 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 3659 . . . . . . . . . . . . . . . . . 18  |-  ( U  i^i  ( B [,] C ) )  C_  U
178 simprl 756 . . . . . . . . . . . . . . . . . 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 3440 . . . . . . . . . . . . . . . . 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 728 . . . . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . . . . 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 3443 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  w  e.  RR )
184183adantrr 715 . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . 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 761 . . . . . . . . . . . . . . . . . . . . . 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 11304 . . . . . . . . . . . . . . . . . . . . 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 9653 . . . . . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . . . . . . 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 728 . . . . . . . . . . . . . . . . . . . . . 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 728 . . . . . . . . . . . . . . . . . . . . . 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 10544 . . . . . . . . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . . . . . . . . . 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 4435 . . . . . . . . . . . . . . . . . . . 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 11333 . . . . . . . . . . . . . . . . . . . 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 9774 . . . . . . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . . . . . . . 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 9669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  -  r )  e.  RR  ->  ( S  -  r )  e.  RR* )
200 rexr 9669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  +  r )  e.  RR  ->  ( S  +  r )  e.  RR* )
201 elioo2 11623 . . . . . . . . . . . . . . . . . . . . 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 475 . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . 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 1180 . . . . . . . . . . . . . . . . . 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 3443 . . . . . . . . . . . . . . . . 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 3627 . . . . . . . . . . . . . . . 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 3443 . . . . . . . . . . . . . . 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 613 . . . . . . . . . . . . . 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 724 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  r  e.  RR+ )  /\  ( ( S  -  r ) (,) ( S  +  r )
)  C_  V )  /\  w  e.  ( U  i^i  ( B [,] C ) ) )  ->  ( S  -  r )  e.  RR )
211183, 210lenltd 9763 . . . . . . . . . . . . 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 2818 . . . . . . . . . . 11  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  ->  A. w  e.  ( U  i^i  ( B [,] C ) ) w  <_  ( S  -  r ) )
21418ad2antrr 724 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( U  i^i  ( B [,] C ) ) 
C_  RR )
21530ad2antrr 724 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( U  i^i  ( B [,] C ) )  =/=  (/) )
21641ad2antrr 724 . . . . . . . . . . . 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 463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  -> 
( S  -  r
)  e.  RR )
218 suprleub 10547 . . . . . . . . . . . 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 1233 . . . . . . . . . . 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 4428 . . . . . . . . 9  |-  ( ( ( ph  /\  r  e.  RR+ )  /\  (
( S  -  r
) (,) ( S  +  r ) ) 
C_  V )  ->  S  <_  ( S  -  r ) )
222221ex 432 . . . . . . . 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 2860 . . . . 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 21288 . . . . . . . 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 1313 . . . . . . 7  |-  ( ( V  e.  ( topGen ` 
ran  (,) )  /\  S  e.  V )  ->  E. r  e.  RR+  ( S (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V )
229228ex 432 . . . . . 6  |-  ( V  e.  ( topGen `  ran  (,) )  ->  ( S  e.  V  ->  E. r  e.  RR+  ( S (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  V )
)
230226, 229syl 17 . . . . 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 488 . . . 4  |-  ( -.  ( S  e.  U  \/  S  e.  V
)  <->  ( -.  S  e.  U  /\  -.  S  e.  V ) )
233160, 231, 232sylanbrc 662 . . 3  |-  ( ph  ->  -.  ( S  e.  U  \/  S  e.  V ) )
234 elun 3584 . . 3  |-  ( S  e.  ( U  u.  V )  <->  ( S  e.  U  \/  S  e.  V ) )
235233, 234sylnibr 303 . 2  |-  ( ph  ->  -.  S  e.  ( U  u.  V ) )
236 elicc2 11643 . . . . . 6  |-  ( ( B  e.  RR  /\  C  e.  RR )  ->  ( S  e.  ( B [,] C )  <-> 
( S  e.  RR  /\  B  <_  S  /\  S  <_  C ) ) )
23721, 23, 236syl2anc 659 . . . . 5  |-  ( ph  ->  ( S  e.  ( B [,] C )  <-> 
( S  e.  RR  /\  B  <_  S  /\  S  <_  C ) ) )
23844, 65, 119, 237mpbir3and 1180 . . . 4  |-  ( ph  ->  S  e.  ( B [,] C ) )
23915, 238sseldd 3443 . . 3  |-  ( ph  ->  S  e.  A )
240 ssel 3436 . . 3  |-  ( A 
C_  ( U  u.  V )  ->  ( S  e.  A  ->  S  e.  ( U  u.  V ) ) )
241239, 240syl5com 28 . 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 366    /\ wa 367    /\ w3a 974    = wceq 1405    e. wcel 1842    =/= wne 2598   A.wral 2754   E.wrex 2755    \ cdif 3411    u. cun 3412    i^i cin 3413    C_ wss 3414   (/)c0 3738   class class class wbr 4395    X. cxp 4821   ran crn 4824    |` cres 4825    o. ccom 4827   ` cfv 5569  (class class class)co 6278   supcsup 7934   RRcr 9521    + caddc 9525   -oocmnf 9656   RR*cxr 9657    < clt 9658    <_ cle 9659    - cmin 9841    / cdiv 10247   2c2 10626   RR+crp 11265   (,)cioo 11582   [,]cicc 11585   abscabs 13216   topGenctg 15052   *Metcxmt 18723   ballcbl 18725   MetOpencmopn 18728   Topctop 19686
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574  ax-cnex 9578  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-mulcom 9586  ax-addass 9587  ax-mulass 9588  ax-distr 9589  ax-i2m1 9590  ax-1ne0 9591  ax-1rid 9592  ax-rnegex 9593  ax-rrecex 9594  ax-cnre 9595  ax-pre-lttri 9596  ax-pre-lttrn 9597  ax-pre-ltadd 9598  ax-pre-mulgt0 9599  ax-pre-sup 9600
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2759  df-rex 2760  df-reu 2761  df-rmo 2762  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-pss 3430  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-tp 3977  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-tr 4490  df-eprel 4734  df-id 4738  df-po 4744  df-so 4745  df-fr 4782  df-we 4784  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-pred 5367  df-ord 5413  df-on 5414  df-lim 5415  df-suc 5416  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-riota 6240  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-om 6684  df-1st 6784  df-2nd 6785  df-wrecs 7013  df-recs 7075  df-rdg 7113  df-er 7348  df-map 7459  df-en 7555  df-dom 7556  df-sdom 7557  df-sup 7935  df-pnf 9660  df-mnf 9661  df-xr 9662  df-ltxr 9663  df-le 9664  df-sub 9843  df-neg 9844  df-div 10248  df-nn 10577  df-2 10635  df-3 10636  df-n0 10837  df-z 10906  df-uz 11128  df-q 11228  df-rp 11266  df-xneg 11371  df-xadd 11372  df-xmul 11373  df-ioo 11586  df-icc 11589  df-seq 12152  df-exp 12211  df-cj 13081  df-re 13082  df-im 13083  df-sqrt 13217  df-abs 13218  df-topgen 15058  df-psmet 18731  df-xmet 18732  df-met 18733  df-bl 18734  df-mopn 18735  df-top 19691  df-bases 19693  df-topon 19694
This theorem is referenced by:  reconn  21625
  Copyright terms: Public domain W3C validator