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

Theorem ptrecube 31854
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 12185 . . . . 5  |-  ( 1 ... N )  e. 
Fin
3 retop 21769 . . . . . 6  |-  ( topGen ` 
ran  (,) )  e.  Top
4 fnconstg 5785 . . . . . 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 2422 . . . . . 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 20572 . . . . 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 676 . . . 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 2451 . . 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 2500 . 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 19967 . . 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 20574 . . . . 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 5888 . . . . . . . . . . . . . . 15  |-  ( topGen ` 
ran  (,) )  e.  _V
1413fvconst2 6132 . . . . . . . . . . . . . 14  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  =  ( topGen ` 
ran  (,) ) )
1514eleq2d 2492 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... N )  ->  (
( g `  n
)  e.  ( ( ( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) `  n
)  <->  ( g `  n )  e.  (
topGen `  ran  (,) )
) )
1615ralbiia 2855 . . . . . . . . . . . 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 7531 . . . . . . . . . . . . . 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 1022 . . . . . . . . . . . . 13  |-  ( P  e.  X_ n  e.  ( 1 ... N ) ( g `  n
)  ->  A. n  e.  ( 1 ... N
) ( P `  n )  e.  ( g `  n ) )
19 r19.26 2955 . . . . . . . . . . . . . 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 21770 . . . . . . . . . . . . . . . . . . . . 21  |-  RR  =  U. ( topGen `  ran  (,) )
2120eltopss 19924 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  ( g `
 n )  e.  ( topGen `  ran  (,) )
)  ->  ( g `  n )  C_  RR )
223, 21mpan 674 . . . . . . . . . . . . . . . . . . 19  |-  ( ( g `  n )  e.  ( topGen `  ran  (,) )  ->  ( g `  n )  C_  RR )
2322sselda 3464 . . . . . . . . . . . . . . . . . 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 21796 . . . . . . . . . . . . . . . . . . 19  |-  D  e.  ( *Met `  RR )
26 eqid 2422 . . . . . . . . . . . . . . . . . . . . 21  |-  ( MetOpen `  D )  =  (
MetOpen `  D )
2724, 26tgioo 21801 . . . . . . . . . . . . . . . . . . . 20  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  D )
2827mopni2 21495 . . . . . . . . . . . . . . . . . . 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 1347 . . . . . . . . . . . . . . . . . 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 2983 . . . . . . . . . . . . . . . . . 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 668 . . . . . . . . . . . . . . . . 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 2818 . . . . . . . . . . . . . . . 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 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( h `  n )  ->  (
( P `  n
) ( ball `  D
) y )  =  ( ( P `  n ) ( ball `  D ) ( h `
 n ) ) )
3433sseq1d 3491 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( h `  n )  ->  (
( ( P `  n ) ( ball `  D ) y ) 
C_  ( g `  n )  <->  ( ( P `  n )
( ball `  D )
( h `  n
) )  C_  (
g `  n )
) )
3534anbi2d 708 . . . . . . . . . . . . . . . . 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 7818 . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . 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 11307 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR+
3938a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : ( 1 ... N ) --> RR+  /\  ( 1 ... N
)  =  (/) )  -> 
1  e.  RR+ )
40 frn 5749 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h : ( 1 ... N ) --> RR+  ->  ran  h  C_  RR+ )
4140adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  ->  ran  h  C_  RR+ )
42 ffn 5743 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h : ( 1 ... N ) --> RR+  ->  h  Fn  ( 1 ... N ) )
43 fnfi 7852 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h  Fn  ( 1 ... N )  /\  ( 1 ... N
)  e.  Fin )  ->  h  e.  Fin )
4442, 2, 43sylancl 666 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h : ( 1 ... N ) --> RR+  ->  h  e.  Fin )
45 rnfi 7860 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h  e.  Fin  ->  ran  h  e.  Fin )
4644, 45syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h : ( 1 ... N ) --> RR+  ->  ran  h  e.  Fin )
4746adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  ->  ran  h  e.  Fin )
48 dm0rn0 5067 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  h  =  (/)  <->  ran  h  =  (/) )
49 fdm 5747 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( h : ( 1 ... N ) --> RR+  ->  dom  h  =  ( 1 ... N ) )
5049eqeq1d 2424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( h : ( 1 ... N ) --> RR+  ->  ( dom  h  =  (/)  <->  (
1 ... N )  =  (/) ) )
5148, 50syl5bbr 262 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( h : ( 1 ... N ) --> RR+  ->  ( ran  h  =  (/)  <->  (
1 ... N )  =  (/) ) )
5251necon3abid 2670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h : ( 1 ... N ) --> RR+  ->  ( ran  h  =/=  (/)  <->  -.  (
1 ... N )  =  (/) ) )
5352biimpar 487 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  ->  ran  h  =/=  (/) )
54 rpssre 11313 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR+  C_  RR
5540, 54syl6ss 3476 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( h : ( 1 ... N ) --> RR+  ->  ran  h  C_  RR )
5655adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  ->  ran  h  C_  RR )
57 ltso 9715 . . . . . . . . . . . . . . . . . . . . . 22  |-  <  Or  RR
58 fiinfcl 8020 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (  <  Or  RR  /\  ( ran  h  e.  Fin  /\ 
ran  h  =/=  (/)  /\  ran  h  C_  RR ) )  -> inf ( ran  h ,  RR ,  <  )  e.  ran  h )
5957, 58mpan 674 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ran  h  e.  Fin  /\ 
ran  h  =/=  (/)  /\  ran  h  C_  RR )  -> inf ( ran  h ,  RR ,  <  )  e.  ran  h )
6047, 53, 56, 59syl3anc 1264 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  -> inf ( ran  h ,  RR ,  <  )  e.  ran  h )
6141, 60sseldd 3465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h : ( 1 ... N ) --> RR+  /\ 
-.  ( 1 ... N )  =  (/) )  -> inf ( ran  h ,  RR ,  <  )  e.  RR+ )
6239, 61ifclda 3941 . . . . . . . . . . . . . . . . . 18  |-  ( h : ( 1 ... N ) --> RR+  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  ) )  e.  RR+ )
6362adantr 466 . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  e.  RR+ )
6564rpxrd 11343 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  e.  RR* )
66 ffvelrn 6032 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ( h `  n )  e.  RR+ )
6766rpxrd 11343 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ( h `  n )  e.  RR* )
68 ne0i 3767 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( n  e.  ( 1 ... N )  ->  (
1 ... N )  =/=  (/) )
69 ifnefalse 3921 . . . . . . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  = inf ( ran  h ,  RR ,  <  ) )
7255adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ran  h  C_  RR )
73 0re 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  RR
74 rpge0 11315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  RR+  ->  0  <_ 
y )
7574rgen 2785 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  A. y  e.  RR+  0  <_  y
76 ssralv 3525 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ran  h  C_  RR+  ->  ( A. y  e.  RR+  0  <_  y  ->  A. y  e.  ran  h 0  <_ 
y ) )
7740, 75, 76mpisyl 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h : ( 1 ... N ) --> RR+  ->  A. y  e.  ran  h
0  <_  y )
78 breq1 4423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  =  0  ->  (
x  <_  y  <->  0  <_  y ) )
7978ralbidv 2864 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  =  0  ->  ( A. y  e.  ran  h  x  <_  y  <->  A. y  e.  ran  h 0  <_ 
y ) )
8079rspcev 3182 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( h : ( 1 ... N ) --> RR+  ->  E. x  e.  RR  A. y  e.  ran  h  x  <_  y )
8281adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  E. x  e.  RR  A. y  e.  ran  h  x  <_  y )
83 fnfvelrn 6031 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h  Fn  ( 1 ... N )  /\  n  e.  ( 1 ... N ) )  ->  ( h `  n )  e.  ran  h )
8442, 83sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  ( h `  n )  e.  ran  h )
85 infrelb 10597 . . . . . . . . . . . . . . . . . . . . . . . . 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 1264 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  -> inf ( ran  h ,  RR ,  <  )  <_  ( h `  n
) )
8771, 86eqbrtrd 4441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( h : ( 1 ... N ) --> RR+  /\  n  e.  ( 1 ... N ) )  ->  if ( ( 1 ... N )  =  (/) ,  1 , inf ( ran  h ,  RR ,  <  )
)  <_  ( h `  n ) )
8865, 67, 87jca31 536 . . . . . . . . . . . . . . . . . . . . . 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 21425 . . . . . . . . . . . . . . . . . . . . . . . . 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 1206 . . . . . . . . . . . . . . . . . . . . . . . 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 684 . . . . . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . . . . . 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 3471 . . . . . . . . . . . . . . . . . . . . 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 606 . . . . . . . . . . . . . . . . . . 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 2833 . . . . . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . . . . . 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 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ball `  D )  =  (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) )
10099oveqi 6315 . . . . . . . . . . . . . . . . . . . . 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 3488 . . . . . . . . . . . . . . . . . . . 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 2856 . . . . . . . . . . . . . . . . . . 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 1751 . . . . . . . . . . . . . . . . . . 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 1692 . . . . . . . . . . . . . . . . . 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 6310 . . . . . . . . . . . . . . . . . . . 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 3491 . . . . . . . . . . . . . . . . . . 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 2864 . . . . . . . . . . . . . . . . . 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 3177 . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . 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 1766 . . . . . . . . . . . . . . 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 216 . . . . . . . . . . . . 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 476 . . . . . . . . . . . 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 474 . . . . . . . . . . 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 7540 . . . . . . . . . . . . 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 3471 . . . . . . . . . . . . . 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 2899 . . . . . . . . . . 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 606 . . . . . . . . 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 2495 . . . . . . . . . . 11  |-  ( z  =  X_ n  e.  ( 1 ... N ) ( g `  n
)  ->  ( P  e.  z  <->  P  e.  X_ n  e.  ( 1 ... N
) ( g `  n ) ) )
123 sseq1 3485 . . . . . . . . . . 11  |-  ( z  =  X_ n  e.  ( 1 ... N ) ( g `  n
)  ->  ( z  C_  S  <->  X_ n  e.  ( 1 ... N ) ( g `  n
)  C_  S )
)
124122, 123anbi12d 715 . . . . . . . . . 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 318 . . . . . . . . 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 225 . . . . . . . 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 1027 . . . . . . 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 430 . . . . . 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 1766 . . . . 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 198 . . . 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 2911 . . 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 474 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 370    /\ w3a 982    = wceq 1437   E.wex 1659    e. wcel 1868   {cab 2407    =/= wne 2618   A.wral 2775   E.wrex 2776   _Vcvv 3081    \ cdif 3433    C_ wss 3436   (/)c0 3761   ifcif 3909   {csn 3996   U.cuni 4216   class class class wbr 4420    Or wor 4770    X. cxp 4848   dom cdm 4850   ran crn 4851    |` cres 4852    o. ccom 4854    Fn wfn 5593   -->wf 5594   ` cfv 5598  (class class class)co 6302   X_cixp 7527   Fincfn 7574  infcinf 7958   RRcr 9539   0cc0 9540   1c1 9541   RR*cxr 9675    < clt 9676    <_ cle 9677    - cmin 9861   RR+crp 11303   (,)cioo 11636   ...cfz 11785   abscabs 13286   topGenctg 15324   Xt_cpt 15325   *Metcxmt 18943   ballcbl 18945   MetOpencmopn 18948   Topctop 19904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-cnex 9596  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616  ax-pre-mulgt0 9617  ax-pre-sup 9618
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-om 6704  df-1st 6804  df-2nd 6805  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-map 7479  df-ixp 7528  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-sup 7959  df-inf 7960  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-sub 9863  df-neg 9864  df-div 10271  df-nn 10611  df-2 10669  df-3 10670  df-n0 10871  df-z 10939  df-uz 11161  df-q 11266  df-rp 11304  df-xneg 11410  df-xadd 11411  df-xmul 11412  df-ioo 11640  df-fz 11786  df-seq 12214  df-exp 12273  df-cj 13151  df-re 13152  df-im 13153  df-sqrt 13287  df-abs 13288  df-topgen 15330  df-pt 15331  df-psmet 18950  df-xmet 18951  df-met 18952  df-bl 18953  df-mopn 18954  df-top 19908  df-bases 19909  df-topon 19910
This theorem is referenced by:  poimirlem29  31883
  Copyright terms: Public domain W3C validator