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 biimtrdi 
 |-  ( 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 biimtrrid 
 |-  ( 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 biimtrrid 
 |-  ( 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 ) )