Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ptrecube Structured version   Visualization version   Unicode version

Theorem ptrecube 31985
Description: Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020.) (Proof shortened by AV, 28-Sep-2020.)
Hypotheses
Ref Expression
ptrecube.r  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
ptrecube.d  |-  D  =  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )
Assertion
Ref Expression
ptrecube  |-  ( ( S  e.  R  /\  P  e.  S )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  S )
Distinct variable groups:    n, d, N    P, d, n    S, d, n
Allowed substitution hints:    D( n, d)    R( n, d)

Proof of Theorem ptrecube
Dummy variables  g  h  w  x  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptrecube.r . . . 4  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
2 fzfi 12217 . . . . 5  |-  ( 1 ... N )  e. 
Fin
3 retop 21831 . . . . . 6  |-  ( topGen ` 
ran  (,) )  e.  Top
4 fnconstg 5794 . . . . . 6  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  ( (
1 ... N )  X. 
{ ( topGen `  ran  (,) ) } )  Fn  ( 1 ... N
) )
53, 4ax-mp 5 . . . . 5  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } )  Fn  ( 1 ... N )
6 eqid 2462 . . . . . 6  |-  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) }  =  {
x  |  E. h
( ( h  Fn  ( 1 ... N
)  /\  A. n  e.  ( 1 ... N
) ( h `  n )  e.  ( ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  /\  E. w  e.  Fin  A. n  e.  ( ( 1 ... N )  \  w
) ( h `  n )  =  U. ( ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) `  n ) )  /\  x  =  X_ n  e.  ( 1 ... N
) ( h `  n ) ) }
76ptval 20634 . . . . 5  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } )  Fn  (
1 ... N ) )  ->  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )  =  ( topGen `  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) } ) )
82, 5, 7mp2an 683 . . . 4  |-  ( Xt_ `  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) )  =  ( topGen `  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) } )
91, 8eqtri 2484 . . 3  |-  R  =  ( topGen `  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) } )
109eleq2i 2532 . 2  |-  ( S  e.  R  <->  S  e.  ( topGen `  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) } ) )
11 tg2 20029 . . 3  |-  ( ( S  e.  ( topGen `  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) } )  /\  P  e.  S )  ->  E. z  e.  {
x  |  E. h
( ( h  Fn  ( 1 ... N
)  /\  A. n  e.  ( 1 ... N
) ( h `  n )  e.  ( ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  /\  E. w  e.  Fin  A. n  e.  ( ( 1 ... N )  \  w
) ( h `  n )  =  U. ( ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) `  n ) )  /\  x  =  X_ n  e.  ( 1 ... N
) ( h `  n ) ) }  ( P  e.  z  /\  z  C_  S
) )
126elpt 20636 . . . . 5  |-  ( z  e.  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) }  <->  E. g
( ( g  Fn  ( 1 ... N
)  /\  A. n  e.  ( 1 ... N
) ( g `  n )  e.  ( ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  /\  E. z  e.  Fin  A. n  e.  ( ( 1 ... N )  \  z
) ( g `  n )  =  U. ( ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) `  n ) )  /\  z  =  X_ n  e.  ( 1 ... N
) ( g `  n ) ) )
13 fvex 5898 . . . . . . . . . . . . . . 15  |-  ( topGen ` 
ran  (,) )  e.  _V
1413fvconst2 6144 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  =  ( topGen ` 
ran  (,) ) )
1514eleq2d 2525 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... N )  ->  (
( g `  n
)  e.  ( ( ( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) `  n
)  <->  ( g `  n )  e.  (
topGen `  ran  (,) )
) )
1615ralbiia 2830 . . . . . . . . . . . 12  |-  ( A. n  e.  ( 1 ... N ) ( g `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  <->  A. n  e.  ( 1 ... N
) ( g `  n )  e.  (
topGen `  ran  (,) )
)
17 elixp2 7552 . . . . . . . . . . . . . 14  |-  ( P  e.  X_ n  e.  ( 1 ... N ) ( g `  n
)  <->  ( P  e. 
_V  /\  P  Fn  ( 1 ... N
)  /\  A. n  e.  ( 1 ... N
) ( P `  n )  e.  ( g `  n ) ) )
1817simp3bi 1031 . . . . . . . . . . . . 13  |-  ( P  e.  X_ n  e.  ( 1 ... N ) ( g `  n
)  ->  A. n  e.  ( 1 ... N
) ( P `  n )  e.  ( g `  n ) )
19 r19.26 2929 . . . . . . . . . . . . . 14  |-  ( A. n  e.  ( 1 ... N ) ( ( g `  n
)  e.  ( topGen ` 
ran  (,) )  /\  ( P `  n )  e.  ( g `  n
) )  <->  ( A. n  e.  ( 1 ... N ) ( g `  n )  e.  ( topGen `  ran  (,) )  /\  A. n  e.  ( 1 ... N
) ( P `  n )  e.  ( g `  n ) ) )
20 uniretop 21832 . . . . . . . . . . . . . . . . . . . . 21  |-  RR  =  U. ( topGen `  ran  (,) )
2120eltopss 19986 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( g `
 n )  e.  ( topGen `  ran  (,) )
)  ->  ( g `  n )  C_  RR )
223, 21mpan 681 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g `  n )  e.  ( topGen `  ran  (,) )  ->  ( g `  n )  C_  RR )
2322sselda 3444 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( g `  n
)  e.  ( topGen ` 
ran  (,) )  /\  ( P `  n )  e.  ( g `  n
) )  ->  ( P `  n )  e.  RR )
24 ptrecube.d . . . . . . . . . . . . . . . . . . . 20  |-  D  =  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )
2524rexmet 21858 . . . . . . . . . . . . . . . . . . 19  |-  D  e.  ( *Met `  RR )
26 eqid 2462 . . . . . . . . . . . . . . . . . . . . 21  |-  ( MetOpen `  D )  =  (
MetOpen `  D )
2724, 26tgioo 21863 . . . . . . . . . . . . . . . . . . . 20  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  D )
2827mopni2 21557 . . . . . . . . . . . . . . . . . . 19  |-  ( ( D  e.  ( *Met `  RR )  /\  ( g `  n )  e.  (
topGen `  ran  (,) )  /\  ( P `  n
)  e.  ( g `
 n ) )  ->  E. y  e.  RR+  ( ( P `  n ) ( ball `  D ) y ) 
C_  ( g `  n ) )
2925, 28mp3an1 1360 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( g `  n
)  e.  ( topGen ` 
ran  (,) )  /\  ( P `  n )  e.  ( g `  n
) )  ->  E. y  e.  RR+  ( ( P `
 n ) (
ball `  D )
y )  C_  (
g `  n )
)
30 r19.42v 2957 . . . . . . . . . . . . . . . . . 18  |-  ( E. y  e.  RR+  (
( P `  n
)  e.  RR  /\  ( ( P `  n ) ( ball `  D ) y ) 
C_  ( g `  n ) )  <->  ( ( P `  n )  e.  RR  /\  E. y  e.  RR+  ( ( P `
 n ) (
ball `  D )
y )  C_  (
g `  n )
) )
3123, 29, 30sylanbrc 675 . . . . . . . . . . . . . . . . 17  |-  ( ( ( g `  n
)  e.  ( topGen ` 
ran  (,) )  /\  ( P `  n )  e.  ( g `  n
) )  ->  E. y  e.  RR+  ( ( P `
 n )  e.  RR  /\  ( ( P `  n ) ( ball `  D
) y )  C_  ( g `  n
) ) )
3231ralimi 2793 . . . . . . . . . . . . . . . 16  |-  ( A. n  e.  ( 1 ... N ) ( ( g `  n
)  e.  ( topGen ` 
ran  (,) )  /\  ( P `  n )  e.  ( g `  n
) )  ->  A. n  e.  ( 1 ... N
) E. y  e.  RR+  ( ( P `  n )  e.  RR  /\  ( ( P `  n ) ( ball `  D ) y ) 
C_  ( g `  n ) ) )
33 oveq2 6323 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( h `  n )  ->  (
( P `  n
) ( ball `  D
) y )  =  ( ( P `  n ) ( ball `  D ) ( h `
 n ) ) )
3433sseq1d 3471 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( h `  n )  ->  (
( ( P `  n ) ( ball `  D ) y ) 
C_  ( g `  n )  <->  ( ( P `  n )
( ball `  D )
( h `  n
) )  C_  (
g `  n )
) )
3534anbi2d 715 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( h `  n )  ->  (
( ( P `  n )  e.  RR  /\  ( ( P `  n ) ( ball `  D ) y ) 
C_  ( g `  n ) )  <->  ( ( P `  n )  e.  RR  /\  ( ( P `  n ) ( ball `  D
) ( h `  n ) )  C_  ( g `  n
) ) ) )
3635ac6sfi 7841 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1 ... N
)  e.  Fin  /\  A. n  e.  ( 1 ... N ) E. y  e.  RR+  (
( P `  n
)  e.  RR  /\  ( ( P `  n ) ( ball `  D ) y ) 
C_  ( g `  n ) ) )  ->  E. h ( h : ( 1 ... N ) --> RR+  /\  A. n  e.  ( 1 ... N ) ( ( P `  n
)  e.  RR  /\  ( ( P `  n ) ( ball `  D ) ( h `
 n ) ) 
C_  ( g `  n ) ) ) )
372, 32, 36sylancr 674 . . . . . . . . . . . . . . 15  |-  ( A. n  e.  ( 1 ... N ) ( ( g `  n
)  e.  ( topGen ` 
ran  (,) )  /\  ( P `  n )  e.  ( g `  n
) )  ->  E. h
( h : ( 1 ... N ) -->
RR+  /\  A. n  e.  ( 1 ... N
) ( ( P `
 n )  e.  RR  /\  ( ( P `  n ) ( ball `  D
) ( h `  n ) )  C_  ( g `  n
) ) ) )
38 1rp 11335 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR+
3938a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : ( 1 ... N ) --> RR+  /\  ( 1 ... N
)  =  (/) )  -> 
1  e.  RR+ )
40 frn 5758 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h : ( 1 ... N ) --> RR+  ->  ran  h  C_  RR+ )
4140adantr 471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  ->  ran  h  C_  RR+ )
42 ffn 5751 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h : ( 1 ... N ) --> RR+  ->  h  Fn  ( 1 ... N ) )
43 fnfi 7875 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h  Fn  ( 1 ... N )  /\  ( 1 ... N
)  e.  Fin )  ->  h  e.  Fin )
4442, 2, 43sylancl 673 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h : ( 1 ... N ) --> RR+  ->  h  e.  Fin )
45 rnfi 7883 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  e.  Fin  ->  ran  h  e.  Fin )
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h : ( 1 ... N ) --> RR+  ->  ran  h  e.  Fin )
4746adantr 471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  ->  ran  h  e.  Fin )
48 dm0rn0 5070 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  h  =  (/)  <->  ran  h  =  (/) )
49 fdm 5756 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( h : ( 1 ... N ) --> RR+  ->  dom  h  =  ( 1 ... N ) )
5049eqeq1d 2464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h : ( 1 ... N ) --> RR+  ->  ( dom  h  =  (/)  <->  (
1 ... N )  =  (/) ) )
5148, 50syl5bbr 267 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h : ( 1 ... N ) --> RR+  ->  ( ran  h  =  (/)  <->  (
1 ... N )  =  (/) ) )
5251necon3abid 2672 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h : ( 1 ... N ) --> RR+  ->  ( ran  h  =/=  (/)  <->  -.  (
1 ... N )  =  (/) ) )
5352biimpar 492 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  ->  ran  h  =/=  (/) )
54 rpssre 11341 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR+  C_  RR
5540, 54syl6ss 3456 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h : ( 1 ... N ) --> RR+  ->  ran  h  C_  RR )
5655adantr 471 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  ->  ran  h  C_  RR )
57 ltso 9740 . . . . . . . . . . . . . . . . . . . . . 22  |-  <  Or  RR
58 fiinfcl 8043 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (  <  Or  RR  /\  ( ran  h  e.  Fin  /\ 
ran  h  =/=  (/)  /\  ran  h  C_  RR ) )  -> inf ( ran  h ,  RR ,  <  )  e.  ran  h )
5957, 58mpan 681 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ran  h  e.  Fin  /\ 
ran  h  =/=  (/)  /\  ran  h  C_  RR )  -> inf ( ran  h ,  RR ,  <  )  e.  ran  h )
6047, 53, 56, 59syl3anc 1276 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  -> inf ( ran  h ,  RR ,  <  )  e.  ran  h )
6141, 60sseldd 3445 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  -> inf ( ran  h ,  RR ,  <  )  e.  RR+ )
6239, 61ifclda 3925 . . . . . . . . . . . . . . . . . 18  |-  ( h : ( 1 ... N ) --> RR+  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  e.  RR+ )
6362adantr 471 . . . . . . . . . . . . . . . . 17  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
A. n  e.  ( 1 ... N ) ( ( P `  n )  e.  RR  /\  ( ( P `  n ) ( ball `  D ) ( h `
 n ) ) 
C_  ( g `  n ) ) )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  e.  RR+ )
6462adantr 471 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  e.  RR+ )
6564rpxrd 11371 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  e.  RR* )
66 ffvelrn 6043 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ( h `  n )  e.  RR+ )
6766rpxrd 11371 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ( h `  n )  e.  RR* )
68 ne0i 3749 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  e.  ( 1 ... N )  ->  (
1 ... N )  =/=  (/) )
69 ifnefalse 3905 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1 ... N )  =/=  (/)  ->  if (
( 1 ... N
)  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  = inf ( ran  h ,  RR ,  <  ) )
7068, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  ( 1 ... N )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  = inf ( ran  h ,  RR ,  <  ) )
7170adantl 472 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  = inf ( ran  h ,  RR ,  <  ) )
7255adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ran  h  C_  RR )
73 0re 9669 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  RR
74 rpge0 11343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  RR+  ->  0  <_ 
y )
7574rgen 2759 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  A. y  e.  RR+  0  <_  y
76 ssralv 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ran  h  C_  RR+  ->  ( A. y  e.  RR+  0  <_  y  ->  A. y  e.  ran  h 0  <_ 
y ) )
7740, 75, 76mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h : ( 1 ... N ) --> RR+  ->  A. y  e.  ran  h
0  <_  y )
78 breq1 4419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
7978ralbidv 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  0  ->  ( A. y  e.  ran  h  x  <_  y  <->  A. y  e.  ran  h 0  <_ 
y ) )
8079rspcev 3162 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 0  e.  RR  /\  A. y  e.  ran  h
0  <_  y )  ->  E. x  e.  RR  A. y  e.  ran  h  x  <_  y )
8173, 77, 80sylancr 674 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( h : ( 1 ... N ) --> RR+  ->  E. x  e.  RR  A. y  e.  ran  h  x  <_  y )
8281adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  E. x  e.  RR  A. y  e.  ran  h  x  <_  y )
83 fnfvelrn 6042 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  Fn  ( 1 ... N )  /\  n  e.  ( 1 ... N ) )  ->  ( h `  n )  e.  ran  h )
8442, 83sylan 478 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ( h `  n )  e.  ran  h )
85 infrelb 10624 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ran  h  C_  RR  /\ 
E. x  e.  RR  A. y  e.  ran  h  x  <_  y  /\  (
h `  n )  e.  ran  h )  -> inf ( ran  h ,  RR ,  <  )  <_  (
h `  n )
)
8672, 82, 84, 85syl3anc 1276 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  -> inf ( ran  h ,  RR ,  <  )  <_  ( h `  n
) )
8771, 86eqbrtrd 4437 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  <_  ( h `  n ) )
8865, 67, 87jca31 541 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ( ( if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  e.  RR*  /\  ( h `  n
)  e.  RR* )  /\  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  <_  (
h `  n )
) )
89 ssbl 21487 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( D  e.  ( *Met `  RR )  /\  ( P `  n )  e.  RR )  /\  ( if ( ( 1 ... N
)  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  e.  RR*  /\  (
h `  n )  e.  RR* )  /\  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  <_  (
h `  n )
)  ->  ( ( P `  n )
( ball `  D ) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) ) )  C_  ( ( P `  n ) ( ball `  D ) ( h `
 n ) ) )
90893expb 1216 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( D  e.  ( *Met `  RR )  /\  ( P `  n )  e.  RR )  /\  ( ( if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  e.  RR*  /\  ( h `  n
)  e.  RR* )  /\  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  <_  (
h `  n )
) )  ->  (
( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
( P `  n
) ( ball `  D
) ( h `  n ) ) )
9125, 90mpanl1 691 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( P `  n
)  e.  RR  /\  ( ( if ( ( 1 ... N
)  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  e.  RR*  /\  (
h `  n )  e.  RR* )  /\  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  <_  (
h `  n )
) )  ->  (
( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
( P `  n
) ( ball `  D
) ( h `  n ) ) )
9291ancoms 459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( if ( ( 1 ... N
)  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  e.  RR*  /\  (
h `  n )  e.  RR* )  /\  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  <_  (
h `  n )
)  /\  ( P `  n )  e.  RR )  ->  ( ( P `
 n ) (
ball `  D ) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) ) )  C_  ( ( P `  n ) ( ball `  D ) ( h `
 n ) ) )
9388, 92sylan 478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( h : ( 1 ... N ) -->
RR+  /\  n  e.  ( 1 ... N
) )  /\  ( P `  n )  e.  RR )  ->  (
( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
( P `  n
) ( ball `  D
) ( h `  n ) ) )
94 sstr2 3451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
( P `  n
) ( ball `  D
) ( h `  n ) )  -> 
( ( ( P `
 n ) (
ball `  D )
( h `  n
) )  C_  (
g `  n )  ->  ( ( P `  n ) ( ball `  D ) if ( ( 1 ... N
)  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )
) )
9593, 94syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( h : ( 1 ... N ) -->
RR+  /\  n  e.  ( 1 ... N
) )  /\  ( P `  n )  e.  RR )  ->  (
( ( P `  n ) ( ball `  D ) ( h `
 n ) ) 
C_  ( g `  n )  ->  (
( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )
) )
9695expimpd 612 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ( ( ( P `  n )  e.  RR  /\  (
( P `  n
) ( ball `  D
) ( h `  n ) )  C_  ( g `  n
) )  ->  (
( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )
) )
9796ralimdva 2808 . . . . . . . . . . . . . . . . . 18  |-  ( h : ( 1 ... N ) --> RR+  ->  ( A. n  e.  ( 1 ... N ) ( ( P `  n )  e.  RR  /\  ( ( P `  n ) ( ball `  D ) ( h `
 n ) ) 
C_  ( g `  n ) )  ->  A. n  e.  (
1 ... N ) ( ( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )
) )
9897imp 435 . . . . . . . . . . . . . . . . 17  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
A. n  e.  ( 1 ... N ) ( ( P `  n )  e.  RR  /\  ( ( P `  n ) ( ball `  D ) ( h `
 n ) ) 
C_  ( g `  n ) ) )  ->  A. n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) if ( ( 1 ... N
)  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )
)
9924fveq2i 5891 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ball `  D )  =  (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) )
10099oveqi 6328 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( P `  n ) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  =  ( ( P `  n
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) ) )
101100sseq1i 3468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )  <->  ( ( P `  n
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) ) )  C_  ( g `  n
) )
102101ralbii 2831 . . . . . . . . . . . . . . . . . . 19  |-  ( A. n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )  <->  A. n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) ) )  C_  ( g `  n
) )
103 nfv 1772 . . . . . . . . . . . . . . . . . . 19  |-  F/ d A. n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )
104102, 103nfxfr 1707 . . . . . . . . . . . . . . . . . 18  |-  F/ d A. n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) if ( ( 1 ... N
)  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )
105 oveq2 6323 . . . . . . . . . . . . . . . . . . . 20  |-  ( d  =  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  ->  ( ( P `  n )
( ball `  D )
d )  =  ( ( P `  n
) ( ball `  D
) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) ) )
106105sseq1d 3471 . . . . . . . . . . . . . . . . . . 19  |-  ( d  =  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  ->  ( (
( P `  n
) ( ball `  D
) d )  C_  ( g `  n
)  <->  ( ( P `
 n ) (
ball `  D ) if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) ) )  C_  ( g `  n
) ) )
107106ralbidv 2839 . . . . . . . . . . . . . . . . . 18  |-  ( d  =  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  ->  ( A. n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  ( g `  n
)  <->  A. n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) if ( ( 1 ... N
)  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )
) )
108104, 107rspce 3157 . . . . . . . . . . . . . . . . 17  |-  ( ( if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  e.  RR+  /\ 
A. n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) if ( ( 1 ... N
)  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
) )  C_  (
g `  n )
)  ->  E. d  e.  RR+  A. n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  (
g `  n )
)
10963, 98, 108syl2anc 671 . . . . . . . . . . . . . . . 16  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
A. n  e.  ( 1 ... N ) ( ( P `  n )  e.  RR  /\  ( ( P `  n ) ( ball `  D ) ( h `
 n ) ) 
C_  ( g `  n ) ) )  ->  E. d  e.  RR+  A. n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  ( g `  n
) )
110109exlimiv 1787 . . . . . . . . . . . . . . 15  |-  ( E. h ( h : ( 1 ... N
) --> RR+  /\  A. n  e.  ( 1 ... N
) ( ( P `
 n )  e.  RR  /\  ( ( P `  n ) ( ball `  D
) ( h `  n ) )  C_  ( g `  n
) ) )  ->  E. d  e.  RR+  A. n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  (
g `  n )
)
11137, 110syl 17 . . . . . . . . . . . . . 14  |-  ( A. n  e.  ( 1 ... N ) ( ( g `  n
)  e.  ( topGen ` 
ran  (,) )  /\  ( P `  n )  e.  ( g `  n
) )  ->  E. d  e.  RR+  A. n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  (
g `  n )
)
11219, 111sylbir 218 . . . . . . . . . . . . 13  |-  ( ( A. n  e.  ( 1 ... N ) ( g `  n
)  e.  ( topGen ` 
ran  (,) )  /\  A. n  e.  ( 1 ... N ) ( P `  n )  e.  ( g `  n ) )  ->  E. d  e.  RR+  A. n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  (
g `  n )
)
11318, 112sylan2 481 . . . . . . . . . . . 12  |-  ( ( A. n  e.  ( 1 ... N ) ( g `  n
)  e.  ( topGen ` 
ran  (,) )  /\  P  e.  X_ n  e.  ( 1 ... N ) ( g `  n
) )  ->  E. d  e.  RR+  A. n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  (
g `  n )
)
11416, 113sylanb 479 . . . . . . . . . . 11  |-  ( ( A. n  e.  ( 1 ... N ) ( g `  n
)  e.  ( ( ( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) `  n
)  /\  P  e.  X_ n  e.  ( 1 ... N ) ( g `  n ) )  ->  E. d  e.  RR+  A. n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  (
g `  n )
)
115 ss2ixp 7561 . . . . . . . . . . . . 13  |-  ( A. n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  ( g `  n
)  ->  X_ n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  X_ n  e.  ( 1 ... N
) ( g `  n ) )
116 sstr2 3451 . . . . . . . . . . . . . 14  |-  ( X_ n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  X_ n  e.  ( 1 ... N ) ( g `  n )  ->  ( X_ n  e.  ( 1 ... N
) ( g `  n )  C_  S  -> 
X_ n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) d ) 
C_  S ) )
117116com12 32 . . . . . . . . . . . . 13  |-  ( X_ n  e.  ( 1 ... N ) ( g `  n ) 
C_  S  ->  ( X_ n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  X_ n  e.  ( 1 ... N ) ( g `  n )  ->  X_ n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) d ) 
C_  S ) )
118115, 117syl5 33 . . . . . . . . . . . 12  |-  ( X_ n  e.  ( 1 ... N ) ( g `  n ) 
C_  S  ->  ( A. n  e.  (
1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  ( g `  n
)  ->  X_ n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  S
) )
119118reximdv 2873 . . . . . . . . . . 11  |-  ( X_ n  e.  ( 1 ... N ) ( g `  n ) 
C_  S  ->  ( E. d  e.  RR+  A. n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  (
g `  n )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  S ) )
120114, 119syl5com 31 . . . . . . . . . 10  |-  ( ( A. n  e.  ( 1 ... N ) ( g `  n
)  e.  ( ( ( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) `  n
)  /\  P  e.  X_ n  e.  ( 1 ... N ) ( g `  n ) )  ->  ( X_ n  e.  ( 1 ... N ) ( g `  n ) 
C_  S  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) d ) 
C_  S ) )
121120expimpd 612 . . . . . . . . 9  |-  ( A. n  e.  ( 1 ... N ) ( g `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  -> 
( ( P  e.  X_ n  e.  (
1 ... N ) ( g `  n )  /\  X_ n  e.  ( 1 ... N ) ( g `  n
)  C_  S )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  S ) )
122 eleq2 2529 . . . . . . . . . . 11  |-  ( z  =  X_ n  e.  ( 1 ... N ) ( g `  n
)  ->  ( P  e.  z  <->  P  e.  X_ n  e.  ( 1 ... N
) ( g `  n ) ) )
123 sseq1 3465 . . . . . . . . . . 11  |-  ( z  =  X_ n  e.  ( 1 ... N ) ( g `  n
)  ->  ( z  C_  S  <->  X_ n  e.  ( 1 ... N ) ( g `  n
)  C_  S )
)
124122, 123anbi12d 722 . . . . . . . . . 10  |-  ( z  =  X_ n  e.  ( 1 ... N ) ( g `  n
)  ->  ( ( P  e.  z  /\  z  C_  S )  <->  ( P  e.  X_ n  e.  ( 1 ... N ) ( g `  n
)  /\  X_ n  e.  ( 1 ... N
) ( g `  n )  C_  S
) ) )
125124imbi1d 323 . . . . . . . . 9  |-  ( z  =  X_ n  e.  ( 1 ... N ) ( g `  n
)  ->  ( (
( P  e.  z  /\  z  C_  S
)  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) d ) 
C_  S )  <->  ( ( P  e.  X_ n  e.  ( 1 ... N
) ( g `  n )  /\  X_ n  e.  ( 1 ... N
) ( g `  n )  C_  S
)  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) d ) 
C_  S ) ) )
126121, 125syl5ibrcom 230 . . . . . . . 8  |-  ( A. n  e.  ( 1 ... N ) ( g `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  -> 
( z  =  X_ n  e.  ( 1 ... N ) ( g `  n )  ->  ( ( P  e.  z  /\  z  C_  S )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) d ) 
C_  S ) ) )
1271263ad2ant2 1036 . . . . . . 7  |-  ( ( g  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( g `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. z  e.  Fin  A. n  e.  ( (
1 ... N )  \ 
z ) ( g `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  ->  ( z  = 
X_ n  e.  ( 1 ... N ) ( g `  n
)  ->  ( ( P  e.  z  /\  z  C_  S )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  S
) ) )
128127imp 435 . . . . . 6  |-  ( ( ( g  Fn  (
1 ... N )  /\  A. n  e.  ( 1 ... N ) ( g `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. z  e.  Fin  A. n  e.  ( (
1 ... N )  \ 
z ) ( g `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  z  =  X_ n  e.  ( 1 ... N ) ( g `  n ) )  ->  ( ( P  e.  z  /\  z  C_  S )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  S
) )
129128exlimiv 1787 . . . . 5  |-  ( E. g ( ( g  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( g `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. z  e.  Fin  A. n  e.  ( (
1 ... N )  \ 
z ) ( g `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  z  =  X_ n  e.  ( 1 ... N ) ( g `  n ) )  ->  ( ( P  e.  z  /\  z  C_  S )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N
) ( ( P `
 n ) (
ball `  D )
d )  C_  S
) )
13012, 129sylbi 200 . . . 4  |-  ( z  e.  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) }  ->  (
( P  e.  z  /\  z  C_  S
)  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) d ) 
C_  S ) )
131130rexlimiv 2885 . . 3  |-  ( E. z  e.  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) }  ( P  e.  z  /\  z  C_  S )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n ) ( ball `  D ) d ) 
C_  S )
13211, 131syl 17 . 2  |-  ( ( S  e.  ( topGen `  { x  |  E. h ( ( h  Fn  ( 1 ... N )  /\  A. n  e.  ( 1 ... N ) ( h `  n )  e.  ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )  /\  E. w  e.  Fin  A. n  e.  ( (
1 ... N )  \  w ) ( h `
 n )  = 
U. ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n ) )  /\  x  =  X_ n  e.  ( 1 ... N ) ( h `  n ) ) } )  /\  P  e.  S )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  S )
13310, 132sylanb 479 1  |-  ( ( S  e.  R  /\  P  e.  S )  ->  E. d  e.  RR+  X_ n  e.  ( 1 ... N ) ( ( P `  n
) ( ball `  D
) d )  C_  S )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 375    /\ w3a 991    = wceq 1455   E.wex 1674    e. wcel 1898   {cab 2448    =/= wne 2633   A.wral 2749   E.wrex 2750   _Vcvv 3057    \ cdif 3413    C_ wss 3416   (/)c0 3743   ifcif 3893   {csn 3980   U.cuni 4212   class class class wbr 4416    Or wor 4773    X. cxp 4851   dom cdm 4853   ran crn 4854    |` cres 4855    o. ccom 4857    Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315   X_cixp 7548   Fincfn 7595  infcinf 7981   RRcr 9564   0cc0 9565   1c1 9566   RR*cxr 9700    < clt 9701    <_ cle 9702    - cmin 9886   RR+crp 11331   (,)cioo 11664   ...cfz 11813   abscabs 13346   topGenctg 15385   Xt_cpt 15386   *Metcxmt 19004   ballcbl 19006   MetOpencmopn 19009   Topctop 19966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642  ax-pre-sup 9643
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-map 7500  df-ixp 7549  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-sup 7982  df-inf 7983  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-div 10298  df-nn 10638  df-2 10696  df-3 10697  df-n0 10899  df-z 10967  df-uz 11189  df-q 11294  df-rp 11332  df-xneg 11438  df-xadd 11439  df-xmul 11440  df-ioo 11668  df-fz 11814  df-seq 12246  df-exp 12305  df-cj 13211  df-re 13212  df-im 13213  df-sqrt 13347  df-abs 13348  df-topgen 15391  df-pt 15392  df-psmet 19011  df-xmet 19012  df-met 19013  df-bl 19014  df-mopn 19015  df-top 19970  df-bases 19971  df-topon 19972
This theorem is referenced by:  poimirlem29  32014
  Copyright terms: Public domain W3C validator