Metamath Proof Explorer


Theorem reconnlem2

Description: Lemma for reconn . (Contributed by Jeff Hankins, 17-Aug-2009) (Proof shortened by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses 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 reconnlem2
|- ( ph -> -. A C_ ( U u. V ) )

Proof

Step Hyp Ref Expression
1 reconnlem2.1
 |-  ( ph -> A C_ RR )
2 reconnlem2.2
 |-  ( ph -> U e. ( topGen ` ran (,) ) )
3 reconnlem2.3
 |-  ( ph -> V e. ( topGen ` ran (,) ) )
4 reconnlem2.4
 |-  ( ph -> A. x e. A A. y e. A ( x [,] y ) C_ A )
5 reconnlem2.5
 |-  ( ph -> B e. ( U i^i A ) )
6 reconnlem2.6
 |-  ( ph -> C e. ( V i^i A ) )
7 reconnlem2.7
 |-  ( ph -> ( U i^i V ) C_ ( RR \ A ) )
8 reconnlem2.8
 |-  ( ph -> B <_ C )
9 reconnlem2.9
 |-  S = sup ( ( U i^i ( B [,] C ) ) , RR , < )
10 inss2
 |-  ( U i^i ( B [,] C ) ) C_ ( B [,] C )
11 5 elin2d
 |-  ( ph -> B e. A )
12 6 elin2d
 |-  ( ph -> C e. A )
13 oveq1
 |-  ( x = B -> ( x [,] y ) = ( B [,] y ) )
14 13 sseq1d
 |-  ( x = B -> ( ( x [,] y ) C_ A <-> ( B [,] y ) C_ A ) )
15 oveq2
 |-  ( y = C -> ( B [,] y ) = ( B [,] C ) )
16 15 sseq1d
 |-  ( y = C -> ( ( B [,] y ) C_ A <-> ( B [,] C ) C_ A ) )
17 14 16 rspc2va
 |-  ( ( ( B e. A /\ C e. A ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> ( B [,] C ) C_ A )
18 11 12 4 17 syl21anc
 |-  ( ph -> ( B [,] C ) C_ A )
19 18 1 sstrd
 |-  ( ph -> ( B [,] C ) C_ RR )
20 10 19 sstrid
 |-  ( ph -> ( U i^i ( B [,] C ) ) C_ RR )
21 5 elin1d
 |-  ( ph -> B e. U )
22 1 11 sseldd
 |-  ( ph -> B e. RR )
23 22 rexrd
 |-  ( ph -> B e. RR* )
24 1 12 sseldd
 |-  ( ph -> C e. RR )
25 24 rexrd
 |-  ( ph -> C e. RR* )
26 lbicc2
 |-  ( ( B e. RR* /\ C e. RR* /\ B <_ C ) -> B e. ( B [,] C ) )
27 23 25 8 26 syl3anc
 |-  ( ph -> B e. ( B [,] C ) )
28 21 27 elind
 |-  ( ph -> B e. ( U i^i ( B [,] C ) ) )
29 28 ne0d
 |-  ( ph -> ( U i^i ( B [,] C ) ) =/= (/) )
30 elinel2
 |-  ( w e. ( U i^i ( B [,] C ) ) -> w e. ( B [,] C ) )
31 elicc2
 |-  ( ( B e. RR /\ C e. RR ) -> ( w e. ( B [,] C ) <-> ( w e. RR /\ B <_ w /\ w <_ C ) ) )
32 22 24 31 syl2anc
 |-  ( ph -> ( w e. ( B [,] C ) <-> ( w e. RR /\ B <_ w /\ w <_ C ) ) )
33 simp3
 |-  ( ( w e. RR /\ B <_ w /\ w <_ C ) -> w <_ C )
34 32 33 syl6bi
 |-  ( ph -> ( w e. ( B [,] C ) -> w <_ C ) )
35 30 34 syl5
 |-  ( ph -> ( w e. ( U i^i ( B [,] C ) ) -> w <_ C ) )
36 35 ralrimiv
 |-  ( ph -> A. w e. ( U i^i ( B [,] C ) ) w <_ C )
37 brralrspcev
 |-  ( ( 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 )
38 24 36 37 syl2anc
 |-  ( ph -> E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z )
39 20 29 38 suprcld
 |-  ( ph -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) e. RR )
40 9 39 eqeltrid
 |-  ( ph -> S e. RR )
41 rphalfcl
 |-  ( r e. RR+ -> ( r / 2 ) e. RR+ )
42 ltaddrp
 |-  ( ( S e. RR /\ ( r / 2 ) e. RR+ ) -> S < ( S + ( r / 2 ) ) )
43 40 41 42 syl2an
 |-  ( ( ph /\ r e. RR+ ) -> S < ( S + ( r / 2 ) ) )
44 40 adantr
 |-  ( ( ph /\ r e. RR+ ) -> S e. RR )
45 41 rpred
 |-  ( r e. RR+ -> ( r / 2 ) e. RR )
46 readdcl
 |-  ( ( S e. RR /\ ( r / 2 ) e. RR ) -> ( S + ( r / 2 ) ) e. RR )
47 40 45 46 syl2an
 |-  ( ( ph /\ r e. RR+ ) -> ( S + ( r / 2 ) ) e. RR )
48 44 47 ltnled
 |-  ( ( ph /\ r e. RR+ ) -> ( S < ( S + ( r / 2 ) ) <-> -. ( S + ( r / 2 ) ) <_ S ) )
49 43 48 mpbid
 |-  ( ( ph /\ r e. RR+ ) -> -. ( S + ( r / 2 ) ) <_ S )
50 20 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( U i^i ( B [,] C ) ) C_ RR )
51 29 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( U i^i ( B [,] C ) ) =/= (/) )
52 38 ad2antrr
 |-  ( ( ( 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 )
53 simpr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) )
54 53 elin1d
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. U )
55 47 adantr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. RR )
56 22 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> B e. RR )
57 40 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> S e. RR )
58 20 29 38 28 suprubd
 |-  ( ph -> B <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
59 58 9 breqtrrdi
 |-  ( ph -> B <_ S )
60 59 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> B <_ S )
61 43 adantr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> S < ( S + ( r / 2 ) ) )
62 57 55 61 ltled
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> S <_ ( S + ( r / 2 ) ) )
63 56 57 55 60 62 letrd
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> B <_ ( S + ( r / 2 ) ) )
64 24 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> C e. RR )
65 53 elin2d
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( -oo (,) C ) )
66 eliooord
 |-  ( ( S + ( r / 2 ) ) e. ( -oo (,) C ) -> ( -oo < ( S + ( r / 2 ) ) /\ ( S + ( r / 2 ) ) < C ) )
67 66 simprd
 |-  ( ( S + ( r / 2 ) ) e. ( -oo (,) C ) -> ( S + ( r / 2 ) ) < C )
68 65 67 syl
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) < C )
69 55 64 68 ltled
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) <_ C )
70 elicc2
 |-  ( ( 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 ) ) )
71 56 64 70 syl2anc
 |-  ( ( ( 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 ) ) )
72 55 63 69 71 mpbir3and
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( B [,] C ) )
73 54 72 elind
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( U i^i ( B [,] C ) ) )
74 50 51 52 73 suprubd
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
75 74 9 breqtrrdi
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) <_ S )
76 49 75 mtand
 |-  ( ( ph /\ r e. RR+ ) -> -. ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) )
77 eqid
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
78 77 remetdval
 |-  ( ( ( S + ( r / 2 ) ) e. RR /\ S e. RR ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) = ( abs ` ( ( S + ( r / 2 ) ) - S ) ) )
79 47 44 78 syl2anc
 |-  ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) = ( abs ` ( ( S + ( r / 2 ) ) - S ) ) )
80 44 recnd
 |-  ( ( ph /\ r e. RR+ ) -> S e. CC )
81 45 adantl
 |-  ( ( ph /\ r e. RR+ ) -> ( r / 2 ) e. RR )
82 81 recnd
 |-  ( ( ph /\ r e. RR+ ) -> ( r / 2 ) e. CC )
83 80 82 pncan2d
 |-  ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) - S ) = ( r / 2 ) )
84 83 fveq2d
 |-  ( ( ph /\ r e. RR+ ) -> ( abs ` ( ( S + ( r / 2 ) ) - S ) ) = ( abs ` ( r / 2 ) ) )
85 41 adantl
 |-  ( ( ph /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
86 rpre
 |-  ( ( r / 2 ) e. RR+ -> ( r / 2 ) e. RR )
87 rpge0
 |-  ( ( r / 2 ) e. RR+ -> 0 <_ ( r / 2 ) )
88 86 87 absidd
 |-  ( ( r / 2 ) e. RR+ -> ( abs ` ( r / 2 ) ) = ( r / 2 ) )
89 85 88 syl
 |-  ( ( ph /\ r e. RR+ ) -> ( abs ` ( r / 2 ) ) = ( r / 2 ) )
90 79 84 89 3eqtrd
 |-  ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) = ( r / 2 ) )
91 rphalflt
 |-  ( r e. RR+ -> ( r / 2 ) < r )
92 91 adantl
 |-  ( ( ph /\ r e. RR+ ) -> ( r / 2 ) < r )
93 90 92 eqbrtrd
 |-  ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) < r )
94 77 rexmet
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
95 94 a1i
 |-  ( ( ph /\ r e. RR+ ) -> ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) )
96 rpxr
 |-  ( r e. RR+ -> r e. RR* )
97 96 adantl
 |-  ( ( ph /\ r e. RR+ ) -> r e. RR* )
98 elbl3
 |-  ( ( ( ( ( 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 ) )
99 95 97 44 47 98 syl22anc
 |-  ( ( 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 ) )
100 93 99 mpbird
 |-  ( ( ph /\ r e. RR+ ) -> ( S + ( r / 2 ) ) e. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) )
101 ssel
 |-  ( ( 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 ) ) ) )
102 100 101 syl5com
 |-  ( ( 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 ) ) ) )
103 76 102 mtod
 |-  ( ( ph /\ r e. RR+ ) -> -. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) )
104 103 nrexdv
 |-  ( ph -> -. E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) )
105 40 adantr
 |-  ( ( ph /\ S e. U ) -> S e. RR )
106 105 mnfltd
 |-  ( ( ph /\ S e. U ) -> -oo < S )
107 suprleub
 |-  ( ( ( ( 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 ) )
108 20 29 38 24 107 syl31anc
 |-  ( ph -> ( sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ C <-> A. w e. ( U i^i ( B [,] C ) ) w <_ C ) )
109 36 108 mpbird
 |-  ( ph -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ C )
110 9 109 eqbrtrid
 |-  ( ph -> S <_ C )
111 40 24 leloed
 |-  ( ph -> ( S <_ C <-> ( S < C \/ S = C ) ) )
112 110 111 mpbid
 |-  ( ph -> ( S < C \/ S = C ) )
113 112 ord
 |-  ( ph -> ( -. S < C -> S = C ) )
114 elndif
 |-  ( C e. A -> -. C e. ( RR \ A ) )
115 12 114 syl
 |-  ( ph -> -. C e. ( RR \ A ) )
116 6 elin1d
 |-  ( ph -> C e. V )
117 elin
 |-  ( C e. ( U i^i V ) <-> ( C e. U /\ C e. V ) )
118 7 sseld
 |-  ( ph -> ( C e. ( U i^i V ) -> C e. ( RR \ A ) ) )
119 117 118 syl5bir
 |-  ( ph -> ( ( C e. U /\ C e. V ) -> C e. ( RR \ A ) ) )
120 116 119 mpan2d
 |-  ( ph -> ( C e. U -> C e. ( RR \ A ) ) )
121 115 120 mtod
 |-  ( ph -> -. C e. U )
122 eleq1
 |-  ( S = C -> ( S e. U <-> C e. U ) )
123 122 notbid
 |-  ( S = C -> ( -. S e. U <-> -. C e. U ) )
124 121 123 syl5ibrcom
 |-  ( ph -> ( S = C -> -. S e. U ) )
125 113 124 syld
 |-  ( ph -> ( -. S < C -> -. S e. U ) )
126 125 con4d
 |-  ( ph -> ( S e. U -> S < C ) )
127 126 imp
 |-  ( ( ph /\ S e. U ) -> S < C )
128 mnfxr
 |-  -oo e. RR*
129 elioo2
 |-  ( ( -oo e. RR* /\ C e. RR* ) -> ( S e. ( -oo (,) C ) <-> ( S e. RR /\ -oo < S /\ S < C ) ) )
130 128 25 129 sylancr
 |-  ( ph -> ( S e. ( -oo (,) C ) <-> ( S e. RR /\ -oo < S /\ S < C ) ) )
131 130 adantr
 |-  ( ( ph /\ S e. U ) -> ( S e. ( -oo (,) C ) <-> ( S e. RR /\ -oo < S /\ S < C ) ) )
132 105 106 127 131 mpbir3and
 |-  ( ( ph /\ S e. U ) -> S e. ( -oo (,) C ) )
133 132 ex
 |-  ( ph -> ( S e. U -> S e. ( -oo (,) C ) ) )
134 133 ancld
 |-  ( ph -> ( S e. U -> ( S e. U /\ S e. ( -oo (,) C ) ) ) )
135 elin
 |-  ( S e. ( U i^i ( -oo (,) C ) ) <-> ( S e. U /\ S e. ( -oo (,) C ) ) )
136 retop
 |-  ( topGen ` ran (,) ) e. Top
137 iooretop
 |-  ( -oo (,) C ) e. ( topGen ` ran (,) )
138 inopn
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ U e. ( topGen ` ran (,) ) /\ ( -oo (,) C ) e. ( topGen ` ran (,) ) ) -> ( U i^i ( -oo (,) C ) ) e. ( topGen ` ran (,) ) )
139 136 137 138 mp3an13
 |-  ( U e. ( topGen ` ran (,) ) -> ( U i^i ( -oo (,) C ) ) e. ( topGen ` ran (,) ) )
140 eqid
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
141 77 140 tgioo
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
142 141 mopni2
 |-  ( ( ( ( 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 ) ) )
143 94 142 mp3an1
 |-  ( ( ( 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 ) ) )
144 143 ex
 |-  ( ( 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 ) ) ) )
145 2 139 144 3syl
 |-  ( 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 ) ) ) )
146 135 145 syl5bir
 |-  ( 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 ) ) ) )
147 134 146 syld
 |-  ( ph -> ( S e. U -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) ) )
148 104 147 mtod
 |-  ( ph -> -. S e. U )
149 ltsubrp
 |-  ( ( S e. RR /\ r e. RR+ ) -> ( S - r ) < S )
150 40 149 sylan
 |-  ( ( ph /\ r e. RR+ ) -> ( S - r ) < S )
151 rpre
 |-  ( r e. RR+ -> r e. RR )
152 resubcl
 |-  ( ( S e. RR /\ r e. RR ) -> ( S - r ) e. RR )
153 40 151 152 syl2an
 |-  ( ( ph /\ r e. RR+ ) -> ( S - r ) e. RR )
154 153 44 ltnled
 |-  ( ( ph /\ r e. RR+ ) -> ( ( S - r ) < S <-> -. S <_ ( S - r ) ) )
155 150 154 mpbid
 |-  ( ( ph /\ r e. RR+ ) -> -. S <_ ( S - r ) )
156 77 bl2ioo
 |-  ( ( S e. RR /\ r e. RR ) -> ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( S - r ) (,) ( S + r ) ) )
157 40 151 156 syl2an
 |-  ( ( ph /\ r e. RR+ ) -> ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( S - r ) (,) ( S + r ) ) )
158 157 sseq1d
 |-  ( ( ph /\ r e. RR+ ) -> ( ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V <-> ( ( S - r ) (,) ( S + r ) ) C_ V ) )
159 20 ad3antrrr
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> ( U i^i ( B [,] C ) ) C_ RR )
160 simpr
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w e. ( U i^i ( B [,] C ) ) )
161 159 160 sseldd
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w e. RR )
162 153 ad2antrr
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> ( S - r ) e. RR )
163 18 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( B [,] C ) C_ A )
164 10 163 sstrid
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( U i^i ( B [,] C ) ) C_ A )
165 164 sselda
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w e. A )
166 elndif
 |-  ( w e. A -> -. w e. ( RR \ A ) )
167 165 166 syl
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> -. w e. ( RR \ A ) )
168 7 ad3antrrr
 |-  ( ( ( ( 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 ) )
169 simprl
 |-  ( ( ( ( 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 ) ) )
170 169 elin1d
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. U )
171 simplr
 |-  ( ( ( ( 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 )
172 161 adantrr
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. RR )
173 simprr
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( S - r ) < w )
174 44 ad2antrr
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> S e. RR )
175 simpllr
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> r e. RR+ )
176 175 rpred
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> r e. RR )
177 174 176 readdcld
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( S + r ) e. RR )
178 159 adantrr
 |-  ( ( ( ( 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 )
179 29 ad3antrrr
 |-  ( ( ( ( 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 ) ) =/= (/) )
180 38 ad3antrrr
 |-  ( ( ( ( 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 )
181 178 179 180 169 suprubd
 |-  ( ( ( ( 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 , < ) )
182 181 9 breqtrrdi
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w <_ S )
183 174 175 ltaddrpd
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> S < ( S + r ) )
184 172 174 177 182 183 lelttrd
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w < ( S + r ) )
185 153 ad2antrr
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( S - r ) e. RR )
186 rexr
 |-  ( ( S - r ) e. RR -> ( S - r ) e. RR* )
187 rexr
 |-  ( ( S + r ) e. RR -> ( S + r ) e. RR* )
188 elioo2
 |-  ( ( ( S - r ) e. RR* /\ ( S + r ) e. RR* ) -> ( w e. ( ( S - r ) (,) ( S + r ) ) <-> ( w e. RR /\ ( S - r ) < w /\ w < ( S + r ) ) ) )
189 186 187 188 syl2an
 |-  ( ( ( S - r ) e. RR /\ ( S + r ) e. RR ) -> ( w e. ( ( S - r ) (,) ( S + r ) ) <-> ( w e. RR /\ ( S - r ) < w /\ w < ( S + r ) ) ) )
190 185 177 189 syl2anc
 |-  ( ( ( ( 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 ) ) ) )
191 172 173 184 190 mpbir3and
 |-  ( ( ( ( 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 ) ) )
192 171 191 sseldd
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. V )
193 170 192 elind
 |-  ( ( ( ( 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 ) )
194 168 193 sseldd
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. ( RR \ A ) )
195 194 expr
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> ( ( S - r ) < w -> w e. ( RR \ A ) ) )
196 167 195 mtod
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> -. ( S - r ) < w )
197 161 162 196 nltled
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w <_ ( S - r ) )
198 197 ralrimiva
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> A. w e. ( U i^i ( B [,] C ) ) w <_ ( S - r ) )
199 20 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( U i^i ( B [,] C ) ) C_ RR )
200 29 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( U i^i ( B [,] C ) ) =/= (/) )
201 38 ad2antrr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z )
202 153 adantr
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( S - r ) e. RR )
203 suprleub
 |-  ( ( ( ( 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 ) ) )
204 199 200 201 202 203 syl31anc
 |-  ( ( ( 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 ) ) )
205 198 204 mpbird
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ ( S - r ) )
206 9 205 eqbrtrid
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> S <_ ( S - r ) )
207 206 ex
 |-  ( ( ph /\ r e. RR+ ) -> ( ( ( S - r ) (,) ( S + r ) ) C_ V -> S <_ ( S - r ) ) )
208 158 207 sylbid
 |-  ( ( ph /\ r e. RR+ ) -> ( ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V -> S <_ ( S - r ) ) )
209 155 208 mtod
 |-  ( ( ph /\ r e. RR+ ) -> -. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
210 209 nrexdv
 |-  ( ph -> -. E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
211 141 mopni2
 |-  ( ( ( ( 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 )
212 94 211 mp3an1
 |-  ( ( V e. ( topGen ` ran (,) ) /\ S e. V ) -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
213 212 ex
 |-  ( V e. ( topGen ` ran (,) ) -> ( S e. V -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V ) )
214 3 213 syl
 |-  ( ph -> ( S e. V -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V ) )
215 210 214 mtod
 |-  ( ph -> -. S e. V )
216 ioran
 |-  ( -. ( S e. U \/ S e. V ) <-> ( -. S e. U /\ -. S e. V ) )
217 148 215 216 sylanbrc
 |-  ( ph -> -. ( S e. U \/ S e. V ) )
218 elun
 |-  ( S e. ( U u. V ) <-> ( S e. U \/ S e. V ) )
219 217 218 sylnibr
 |-  ( ph -> -. S e. ( U u. V ) )
220 elicc2
 |-  ( ( B e. RR /\ C e. RR ) -> ( S e. ( B [,] C ) <-> ( S e. RR /\ B <_ S /\ S <_ C ) ) )
221 22 24 220 syl2anc
 |-  ( ph -> ( S e. ( B [,] C ) <-> ( S e. RR /\ B <_ S /\ S <_ C ) ) )
222 40 59 110 221 mpbir3and
 |-  ( ph -> S e. ( B [,] C ) )
223 18 222 sseldd
 |-  ( ph -> S e. A )
224 ssel
 |-  ( A C_ ( U u. V ) -> ( S e. A -> S e. ( U u. V ) ) )
225 223 224 syl5com
 |-  ( ph -> ( A C_ ( U u. V ) -> S e. ( U u. V ) ) )
226 219 225 mtod
 |-  ( ph -> -. A C_ ( U u. V ) )