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 ) ) |