Metamath Proof Explorer

Theorem ptrecube

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)

Ref Expression
Hypotheses ptrecube.r 
|- R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
ptrecube.d 
|- D = ( ( abs o. - ) |` ( RR X. RR ) )
Assertion ptrecube 
|- ( ( S e. R /\ P e. S ) -> E. d e. RR+ X_ n e. ( 1 ... N ) ( ( P ` n ) ( ball ` D ) d ) C_ S )

Proof

Step Hyp Ref Expression
1 ptrecube.r 
 |-  R = ( Xt_ ` ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) )
2 ptrecube.d 
 |-  D = ( ( abs o. - ) |` ( RR X. RR ) )
3 fzfi 
 |-  ( 1 ... N ) e. Fin
4 retop 
 |-  ( topGen ` ran (,) ) e. Top
5 fnconstg 
 |-  ( ( topGen ` ran (,) ) e. Top -> ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) Fn ( 1 ... N ) )
6 4 5 ax-mp 
 |-  ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) Fn ( 1 ... N )
7 eqid 
 |-  { 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 ) ) }
8 7 ptval 
 |-  ( ( ( 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 ) ) } ) )
9 3 6 8 mp2an 
 |-  ( 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 ) ) } )
10 1 9 eqtri 
 |-  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 ) ) } )
11 10 eleq2i 
 |-  ( 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 ) ) } ) )
12 tg2 
 |-  ( ( 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 ) )
13 7 elpt 
 |-  ( 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 ) ) )
14 fvex 
 |-  ( topGen ` ran (,) ) e. _V
15 14 fvconst2 
 |-  ( n e. ( 1 ... N ) -> ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) = ( topGen ` ran (,) ) )
16 15 eleq2d 
 |-  ( n e. ( 1 ... N ) -> ( ( g ` n ) e. ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) <-> ( g ` n ) e. ( topGen ` ran (,) ) ) )
17 16 ralbiia 
 |-  ( A. n e. ( 1 ... N ) ( g ` n ) e. ( ( ( 1 ... N ) X. { ( topGen ` ran (,) ) } ) ` n ) <-> A. n e. ( 1 ... N ) ( g ` n ) e. ( topGen ` ran (,) ) )
18 elixp2 
 |-  ( 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 ) ) )
19 18 simp3bi 
 |-  ( P e. X_ n e. ( 1 ... N ) ( g ` n ) -> A. n e. ( 1 ... N ) ( P ` n ) e. ( g ` n ) )
20 r19.26 
 |-  ( 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 ) ) )
21 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
22 21 eltopss 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ ( g ` n ) e. ( topGen ` ran (,) ) ) -> ( g ` n ) C_ RR )
23 4 22 mpan 
 |-  ( ( g ` n ) e. ( topGen ` ran (,) ) -> ( g ` n ) C_ RR )
24 23 sselda 
 |-  ( ( ( g ` n ) e. ( topGen ` ran (,) ) /\ ( P ` n ) e. ( g ` n ) ) -> ( P ` n ) e. RR )
25 2 rexmet 
 |-  D e. ( *Met ` RR )
26 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
27 2 26 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` D )
28 27 mopni2 
 |-  ( ( 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 ) )
29 25 28 mp3an1 
 |-  ( ( ( 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 
 |-  ( 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 ) ) )
31 24 29 30 sylanbrc 
 |-  ( ( ( 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 ) ) )
32 31 ralimi 
 |-  ( 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 
 |-  ( y = ( h ` n ) -> ( ( P ` n ) ( ball ` D ) y ) = ( ( P ` n ) ( ball ` D ) ( h ` n ) ) )
34 33 sseq1d 
 |-  ( y = ( h ` n ) -> ( ( ( P ` n ) ( ball ` D ) y ) C_ ( g ` n ) <-> ( ( P ` n ) ( ball ` D ) ( h ` n ) ) C_ ( g ` n ) ) )
35 34 anbi2d 
 |-  ( 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 ) ) ) )
36 35 ac6sfi 
 |-  ( ( ( 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 ) ) ) )
37 3 32 36 sylancr 
 |-  ( 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 
 |-  1 e. RR+
39 38 a1i 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ ( 1 ... N ) = (/) ) -> 1 e. RR+ )
40 frn 
 |-  ( h : ( 1 ... N ) --> RR+ -> ran h C_ RR+ )
41 40 adantr 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ -. ( 1 ... N ) = (/) ) -> ran h C_ RR+ )
42 ffn 
 |-  ( h : ( 1 ... N ) --> RR+ -> h Fn ( 1 ... N ) )
43 fnfi 
 |-  ( ( h Fn ( 1 ... N ) /\ ( 1 ... N ) e. Fin ) -> h e. Fin )
44 42 3 43 sylancl 
 |-  ( h : ( 1 ... N ) --> RR+ -> h e. Fin )
45 rnfi 
 |-  ( h e. Fin -> ran h e. Fin )
46 44 45 syl 
 |-  ( h : ( 1 ... N ) --> RR+ -> ran h e. Fin )
47 46 adantr 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ -. ( 1 ... N ) = (/) ) -> ran h e. Fin )
48 dm0rn0 
 |-  ( dom h = (/) <-> ran h = (/) )
49 fdm 
 |-  ( h : ( 1 ... N ) --> RR+ -> dom h = ( 1 ... N ) )
50 49 eqeq1d 
 |-  ( h : ( 1 ... N ) --> RR+ -> ( dom h = (/) <-> ( 1 ... N ) = (/) ) )
51 48 50 bitr3id 
 |-  ( h : ( 1 ... N ) --> RR+ -> ( ran h = (/) <-> ( 1 ... N ) = (/) ) )
52 51 necon3abid 
 |-  ( h : ( 1 ... N ) --> RR+ -> ( ran h =/= (/) <-> -. ( 1 ... N ) = (/) ) )
53 52 biimpar 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ -. ( 1 ... N ) = (/) ) -> ran h =/= (/) )
54 rpssre 
 |-  RR+ C_ RR
55 40 54 sstrdi 
 |-  ( h : ( 1 ... N ) --> RR+ -> ran h C_ RR )
56 55 adantr 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ -. ( 1 ... N ) = (/) ) -> ran h C_ RR )
57 ltso 
 |-  < Or RR
58 fiinfcl 
 |-  ( ( < Or RR /\ ( ran h e. Fin /\ ran h =/= (/) /\ ran h C_ RR ) ) -> inf ( ran h , RR , < ) e. ran h )
59 57 58 mpan 
 |-  ( ( ran h e. Fin /\ ran h =/= (/) /\ ran h C_ RR ) -> inf ( ran h , RR , < ) e. ran h )
60 47 53 56 59 syl3anc 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ -. ( 1 ... N ) = (/) ) -> inf ( ran h , RR , < ) e. ran h )
61 41 60 sseldd 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ -. ( 1 ... N ) = (/) ) -> inf ( ran h , RR , < ) e. RR+ )
62 39 61 ifclda 
 |-  ( h : ( 1 ... N ) --> RR+ -> if ( ( 1 ... N ) = (/) , 1 , inf ( ran h , RR , < ) ) e. RR+ )
63 62 adantr 
 |-  ( ( 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+ )
64 62 adantr 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> if ( ( 1 ... N ) = (/) , 1 , inf ( ran h , RR , < ) ) e. RR+ )
65 64 rpxrd 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> if ( ( 1 ... N ) = (/) , 1 , inf ( ran h , RR , < ) ) e. RR* )
66 ffvelrn 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> ( h ` n ) e. RR+ )
67 66 rpxrd 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> ( h ` n ) e. RR* )
68 ne0i 
 |-  ( n e. ( 1 ... N ) -> ( 1 ... N ) =/= (/) )
69 ifnefalse 
 |-  ( ( 1 ... N ) =/= (/) -> if ( ( 1 ... N ) = (/) , 1 , inf ( ran h , RR , < ) ) = inf ( ran h , RR , < ) )
70 68 69 syl 
 |-  ( n e. ( 1 ... N ) -> if ( ( 1 ... N ) = (/) , 1 , inf ( ran h , RR , < ) ) = inf ( ran h , RR , < ) )
71 70 adantl 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> if ( ( 1 ... N ) = (/) , 1 , inf ( ran h , RR , < ) ) = inf ( ran h , RR , < ) )
72 55 adantr 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> ran h C_ RR )
73 0re 
 |-  0 e. RR
74 rpge0 
 |-  ( y e. RR+ -> 0 <_ y )
75 74 rgen 
 |-  A. y e. RR+ 0 <_ y
76 ssralv 
 |-  ( ran h C_ RR+ -> ( A. y e. RR+ 0 <_ y -> A. y e. ran h 0 <_ y ) )
77 40 75 76 mpisyl 
 |-  ( h : ( 1 ... N ) --> RR+ -> A. y e. ran h 0 <_ y )
78 breq1 
 |-  ( x = 0 -> ( x <_ y <-> 0 <_ y ) )
79 78 ralbidv 
 |-  ( x = 0 -> ( A. y e. ran h x <_ y <-> A. y e. ran h 0 <_ y ) )
80 79 rspcev 
 |-  ( ( 0 e. RR /\ A. y e. ran h 0 <_ y ) -> E. x e. RR A. y e. ran h x <_ y )
81 73 77 80 sylancr 
 |-  ( h : ( 1 ... N ) --> RR+ -> E. x e. RR A. y e. ran h x <_ y )
82 81 adantr 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> E. x e. RR A. y e. ran h x <_ y )
83 fnfvelrn 
 |-  ( ( h Fn ( 1 ... N ) /\ n e. ( 1 ... N ) ) -> ( h ` n ) e. ran h )
84 42 83 sylan 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> ( h ` n ) e. ran h )
85 infrelb 
 |-  ( ( 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 ) )
86 72 82 84 85 syl3anc 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> inf ( ran h , RR , < ) <_ ( h ` n ) )
87 71 86 eqbrtrd 
 |-  ( ( h : ( 1 ... N ) --> RR+ /\ n e. ( 1 ... N ) ) -> if ( ( 1 ... N ) = (/) , 1 , inf ( ran h , RR , < ) ) <_ ( h ` n ) )
88 65 67 87 jca31 
 |-  ( ( 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 
 |-  ( ( ( 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 ) ) )
90 89 3expb 
 |-  ( ( ( 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 ) ) )
91 25 90 mpanl1 
 |-  ( ( ( 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 ) ) )
92 91 ancoms 
 |-  ( ( ( ( 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 ) ) )
93 88 92 sylan 
 |-  ( ( ( 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 
 |-  ( ( ( 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 ) ) )
95 93 94 syl 
 |-  ( ( ( 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 ) ) )
96 95 expimpd 
 |-  ( ( 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 ) ) )
97 96 ralimdva 
 |-  ( 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 ) ) )
98 97 imp 
 |-  ( ( 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 ) )
99 2 fveq2i 
 |-  ( ball ` D ) = ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) )
100 99 oveqi 
 |-  ( ( 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 , < ) ) )
101 100 sseq1i 
 |-  ( ( ( 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 ) )
102 101 ralbii 
 |-  ( 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 
 |-  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 )
104 102 103 nfxfr 
 |-  F/ d A. n e. ( 1 ... N ) ( ( P ` n ) ( ball ` D ) if ( ( 1 ... N ) = (/) , 1 , inf ( ran h , RR , < ) ) ) C_ ( g ` n )
105 oveq2 
 |-  ( 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 , < ) ) ) )
106 105 sseq1d 
 |-  ( 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 ) ) )
107 106 ralbidv 
 |-  ( 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 ) ) )
108 104 107 rspce 
 |-  ( ( 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 ) )
109 63 98 108 syl2anc 
 |-  ( ( 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 ) )
110 109 exlimiv 
 |-  ( 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 ) )
111 37 110 syl 
 |-  ( 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 ) )
112 20 111 sylbir 
 |-  ( ( 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 ) )
113 19 112 sylan2 
 |-  ( ( 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 ) )
114 17 113 sylanb 
 |-  ( ( 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 sstr2 
 |-  ( 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 ) )
116 ss2ixp 
 |-  ( 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 ) )
117 115 116 syl11 
 |-  ( 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 ) )
118 117 reximdv 
 |-  ( 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 ) )
119 114 118 syl5com 
 |-  ( ( 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 ) )
120 119 expimpd 
 |-  ( 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 ) )
121 eleq2 
 |-  ( z = X_ n e. ( 1 ... N ) ( g ` n ) -> ( P e. z <-> P e. X_ n e. ( 1 ... N ) ( g ` n ) ) )
122 sseq1 
 |-  ( z = X_ n e. ( 1 ... N ) ( g ` n ) -> ( z C_ S <-> X_ n e. ( 1 ... N ) ( g ` n ) C_ S ) )
123 121 122 anbi12d 
 |-  ( 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 ) ) )
124 123 imbi1d 
 |-  ( 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 ) ) )
125 120 124 syl5ibrcom 
 |-  ( 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 ) ) )
126 125 3ad2ant2 
 |-  ( ( 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 ) ) )
127 126 imp 
 |-  ( ( ( 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 ) )
128 127 exlimiv 
 |-  ( 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 ) )
129 13 128 sylbi 
 |-  ( 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 ) )
130 129 rexlimiv 
 |-  ( 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 )
131 12 130 syl 
 |-  ( ( 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 )
132 11 131 sylanb 
 |-  ( ( S e. R /\ P e. S ) -> E. d e. RR+ X_ n e. ( 1 ... N ) ( ( P ` n ) ( ball ` D ) d ) C_ S )