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

Theorem poimirlem30 32034
Description: Lemma for poimir 32037 combining poimirlem29 32033 with bwth 20502. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimir.i  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
poimir.r  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
poimir.1  |-  ( ph  ->  F  e.  ( ( Rt  I )  Cn  R
) )
poimirlem30.x  |-  X  =  ( ( F `  ( ( ( 1st `  ( G `  k
) )  oF  +  ( ( ( ( 2nd `  ( G `  k )
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( G `  k )
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  oF  /  ( ( 1 ... N )  X.  { k } ) ) ) `  n )
poimirlem30.2  |-  ( ph  ->  G : NN --> ( ( NN0  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
poimirlem30.3  |-  ( (
ph  /\  k  e.  NN )  ->  ran  ( 1st `  ( G `  k ) )  C_  ( 0..^ k ) )
poimirlem30.4  |-  ( (
ph  /\  ( k  e.  NN  /\  n  e.  ( 1 ... N
)  /\  r  e.  {  <_  ,  `'  <_  } ) )  ->  E. j  e.  ( 0 ... N
) 0 r X )
Assertion
Ref Expression
poimirlem30  |-  ( ph  ->  E. c  e.  I  A. n  e.  (
1 ... N ) A. v  e.  ( Rt  I
) ( c  e.  v  ->  A. r  e.  {  <_  ,  `'  <_  } E. z  e.  v  0 r ( ( F `  z
) `  n )
) )
Distinct variable groups:    f, j,
k, n, z    ph, j, n    j, F, n    j, N, n    ph, k    f, N, k    ph, z    f, F, k, z    z, N   
j, c, k, n, r, v, z, ph    f, c, F, r, v    G, c, f, j, k, n, r, v, z   
I, c, f, j, k, n, r, v, z    N, c, r, v    R, c, f, j, k, n, r, v, z    X, c, f, r, v, z
Allowed substitution hints:    ph( f)    X( j, k, n)

Proof of Theorem poimirlem30
Dummy variables  i  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfzonn0 11988 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0..^ k )  ->  i  e.  NN0 )
21nn0red 10950 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ k )  ->  i  e.  RR )
3 nndivre 10667 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  RR  /\  k  e.  NN )  ->  ( i  /  k
)  e.  RR )
42, 3sylan 479 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
i  /  k )  e.  RR )
5 elfzole1 11955 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0..^ k )  ->  0  <_  i )
62, 5jca 541 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0..^ k )  ->  ( i  e.  RR  /\  0  <_ 
i ) )
7 nnrp 11334 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  k  e.  RR+ )
87rpregt0d 11370 . . . . . . . . . . . . . . 15  |-  ( k  e.  NN  ->  (
k  e.  RR  /\  0  <  k ) )
9 divge0 10496 . . . . . . . . . . . . . . 15  |-  ( ( ( i  e.  RR  /\  0  <_  i )  /\  ( k  e.  RR  /\  0  <  k ) )  ->  0  <_  ( i  /  k ) )
106, 8, 9syl2an 485 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  0  <_  ( i  /  k
) )
11 elfzo0le 11987 . . . . . . . . . . . . . . . 16  |-  ( i  e.  ( 0..^ k )  ->  i  <_  k )
1211adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  i  <_  k )
132adantr 472 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  i  e.  RR )
14 1red 9676 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  1  e.  RR )
157adantl 473 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  k  e.  RR+ )
1613, 14, 15ledivmuld 11414 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
( i  /  k
)  <_  1  <->  i  <_  ( k  x.  1 ) ) )
17 nncn 10639 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  NN  ->  k  e.  CC )
1817mulid1d 9678 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  NN  ->  (
k  x.  1 )  =  k )
1918breq2d 4407 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  NN  ->  (
i  <_  ( k  x.  1 )  <->  i  <_  k ) )
2019adantl 473 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
i  <_  ( k  x.  1 )  <->  i  <_  k ) )
2116, 20bitrd 261 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
( i  /  k
)  <_  1  <->  i  <_  k ) )
2212, 21mpbird 240 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
i  /  k )  <_  1 )
23 0re 9661 . . . . . . . . . . . . . . 15  |-  0  e.  RR
24 1re 9660 . . . . . . . . . . . . . . 15  |-  1  e.  RR
2523, 24elicc2i 11725 . . . . . . . . . . . . . 14  |-  ( ( i  /  k )  e.  ( 0 [,] 1 )  <->  ( (
i  /  k )  e.  RR  /\  0  <_  ( i  /  k
)  /\  ( i  /  k )  <_ 
1 ) )
264, 10, 22, 25syl3anbrc 1214 . . . . . . . . . . . . 13  |-  ( ( i  e.  ( 0..^ k )  /\  k  e.  NN )  ->  (
i  /  k )  e.  ( 0 [,] 1 ) )
2726ancoms 460 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  /\  i  e.  ( 0..^ k ) )  -> 
( i  /  k
)  e.  ( 0 [,] 1 ) )
28 elsni 3985 . . . . . . . . . . . . . 14  |-  ( j  e.  { k }  ->  j  =  k )
2928oveq2d 6324 . . . . . . . . . . . . 13  |-  ( j  e.  { k }  ->  ( i  / 
j )  =  ( i  /  k ) )
3029eleq1d 2533 . . . . . . . . . . . 12  |-  ( j  e.  { k }  ->  ( ( i  /  j )  e.  ( 0 [,] 1
)  <->  ( i  / 
k )  e.  ( 0 [,] 1 ) ) )
3127, 30syl5ibrcom 230 . . . . . . . . . . 11  |-  ( ( k  e.  NN  /\  i  e.  ( 0..^ k ) )  -> 
( j  e.  {
k }  ->  (
i  /  j )  e.  ( 0 [,] 1 ) ) )
3231impr 631 . . . . . . . . . 10  |-  ( ( k  e.  NN  /\  ( i  e.  ( 0..^ k )  /\  j  e.  { k } ) )  -> 
( i  /  j
)  e.  ( 0 [,] 1 ) )
3332adantll 728 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  NN )  /\  (
i  e.  ( 0..^ k )  /\  j  e.  { k } ) )  ->  ( i  /  j )  e.  ( 0 [,] 1
) )
34 poimirlem30.2 . . . . . . . . . . . 12  |-  ( ph  ->  G : NN --> ( ( NN0  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
3534ffvelrnda 6037 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN )  ->  ( G `
 k )  e.  ( ( NN0  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } ) )
36 xp1st 6842 . . . . . . . . . . 11  |-  ( ( G `  k )  e.  ( ( NN0 
^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  -> 
( 1st `  ( G `  k )
)  e.  ( NN0 
^m  ( 1 ... N ) ) )
37 elmapfn 7512 . . . . . . . . . . 11  |-  ( ( 1st `  ( G `
 k ) )  e.  ( NN0  ^m  ( 1 ... N
) )  ->  ( 1st `  ( G `  k ) )  Fn  ( 1 ... N
) )
3835, 36, 373syl 18 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1st `  ( G `  k
) )  Fn  (
1 ... N ) )
39 poimirlem30.3 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ran  ( 1st `  ( G `  k ) )  C_  ( 0..^ k ) )
40 df-f 5593 . . . . . . . . . 10  |-  ( ( 1st `  ( G `
 k ) ) : ( 1 ... N ) --> ( 0..^ k )  <->  ( ( 1st `  ( G `  k ) )  Fn  ( 1 ... N
)  /\  ran  ( 1st `  ( G `  k
) )  C_  (
0..^ k ) ) )
4138, 39, 40sylanbrc 677 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1st `  ( G `  k
) ) : ( 1 ... N ) --> ( 0..^ k ) )
42 vex 3034 . . . . . . . . . . 11  |-  k  e. 
_V
4342fconst 5782 . . . . . . . . . 10  |-  ( ( 1 ... N )  X.  { k } ) : ( 1 ... N ) --> { k }
4443a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1 ... N )  X.  { k } ) : ( 1 ... N ) --> { k } )
45 fzfid 12224 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( 1 ... N )  e. 
Fin )
46 inidm 3632 . . . . . . . . 9  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
4733, 41, 44, 45, 45, 46off 6565 . . . . . . . 8  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) : ( 1 ... N
) --> ( 0 [,] 1 ) )
48 poimir.i . . . . . . . . . 10  |-  I  =  ( ( 0 [,] 1 )  ^m  (
1 ... N ) )
4948eleq2i 2541 . . . . . . . . 9  |-  ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  I  <->  ( ( 1st `  ( G `  k ) )  oF  /  ( ( 1 ... N )  X.  { k } ) )  e.  ( ( 0 [,] 1
)  ^m  ( 1 ... N ) ) )
50 ovex 6336 . . . . . . . . . 10  |-  ( 0 [,] 1 )  e. 
_V
51 ovex 6336 . . . . . . . . . 10  |-  ( 1 ... N )  e. 
_V
5250, 51elmap 7518 . . . . . . . . 9  |-  ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  ( ( 0 [,] 1 )  ^m  ( 1 ... N
) )  <->  ( ( 1st `  ( G `  k ) )  oF  /  ( ( 1 ... N )  X.  { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1
) )
5349, 52bitri 257 . . . . . . . 8  |-  ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  e.  I  <->  ( ( 1st `  ( G `  k ) )  oF  /  ( ( 1 ... N )  X.  { k } ) ) : ( 1 ... N ) --> ( 0 [,] 1
) )
5447, 53sylibr 217 . . . . . . 7  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  e.  I )
55 eqid 2471 . . . . . . 7  |-  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )  =  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )
5654, 55fmptd 6061 . . . . . 6  |-  ( ph  ->  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) : NN --> I )
57 frn 5747 . . . . . 6  |-  ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) : NN --> I  ->  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  C_  I )
5856, 57syl 17 . . . . 5  |-  ( ph  ->  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  C_  I
)
59 ominf 7802 . . . . . . 7  |-  -.  om  e.  Fin
60 nnenom 12231 . . . . . . . . 9  |-  NN  ~~  om
61 enfi 7806 . . . . . . . . 9  |-  ( NN 
~~  om  ->  ( NN  e.  Fin  <->  om  e.  Fin ) )
6260, 61ax-mp 5 . . . . . . . 8  |-  ( NN  e.  Fin  <->  om  e.  Fin )
63 iunid 4324 . . . . . . . . . . 11  |-  U_ c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) { c }  =  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )
6463imaeq2i 5172 . . . . . . . . . 10  |-  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " U_ c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) { c } )  =  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )
65 imaiun 6168 . . . . . . . . . 10  |-  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " U_ c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) { c } )  =  U_ c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" { c } )
66 ovex 6336 . . . . . . . . . . . . 13  |-  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  e. 
_V
6766, 55fnmpti 5716 . . . . . . . . . . . 12  |-  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )  Fn  NN
68 dffn3 5748 . . . . . . . . . . . 12  |-  ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  Fn  NN  <->  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) : NN --> ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )
6967, 68mpbi 213 . . . . . . . . . . 11  |-  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) : NN --> ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )
70 fimacnv 6027 . . . . . . . . . . 11  |-  ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) : NN --> ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  ->  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )  =  NN )
7169, 70ax-mp 5 . . . . . . . . . 10  |-  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )  =  NN
7264, 65, 713eqtr3ri 2502 . . . . . . . . 9  |-  NN  =  U_ c  e.  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )
7372eleq1i 2540 . . . . . . . 8  |-  ( NN  e.  Fin  <->  U_ c  e. 
ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin )
7462, 73bitr3i 259 . . . . . . 7  |-  ( om  e.  Fin  <->  U_ c  e. 
ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin )
7559, 74mtbi 305 . . . . . 6  |-  -.  U_ c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" { c } )  e.  Fin
76 ralnex 2834 . . . . . . . . . . . 12  |-  ( A. k  e.  ( ZZ>= `  i )  -.  (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  <->  -.  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )
7776rexbii 2881 . . . . . . . . . . 11  |-  ( E. i  e.  NN  A. k  e.  ( ZZ>= `  i )  -.  (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  <->  E. i  e.  NN  -.  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )
78 rexnal 2836 . . . . . . . . . . 11  |-  ( E. i  e.  NN  -.  E. k  e.  ( ZZ>= `  i ) ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  =  c  <->  -.  A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )
7977, 78bitri 257 . . . . . . . . . 10  |-  ( E. i  e.  NN  A. k  e.  ( ZZ>= `  i )  -.  (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  <->  -.  A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )
8079ralbii 2823 . . . . . . . . 9  |-  ( A. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) E. i  e.  NN  A. k  e.  ( ZZ>= `  i )  -.  (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  <->  A. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  -.  A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )
81 ralnex 2834 . . . . . . . . 9  |-  ( A. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )  -.  A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  <->  -.  E. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )
8280, 81bitri 257 . . . . . . . 8  |-  ( A. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) E. i  e.  NN  A. k  e.  ( ZZ>= `  i )  -.  (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  <->  -.  E. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )
83 nnuz 11218 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
84 elnnuz 11219 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  NN  <->  i  e.  ( ZZ>= `  1 )
)
85 fzouzsplit 11980 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( ZZ>= `  1
)  ->  ( ZZ>= ` 
1 )  =  ( ( 1..^ i )  u.  ( ZZ>= `  i
) ) )
8684, 85sylbi 200 . . . . . . . . . . . . . . . 16  |-  ( i  e.  NN  ->  ( ZZ>=
`  1 )  =  ( ( 1..^ i )  u.  ( ZZ>= `  i ) ) )
8783, 86syl5eq 2517 . . . . . . . . . . . . . . 15  |-  ( i  e.  NN  ->  NN  =  ( ( 1..^ i )  u.  ( ZZ>=
`  i ) ) )
8887difeq1d 3539 . . . . . . . . . . . . . 14  |-  ( i  e.  NN  ->  ( NN  \  ( 1..^ i ) )  =  ( ( ( 1..^ i )  u.  ( ZZ>= `  i ) )  \ 
( 1..^ i ) ) )
89 uncom 3569 . . . . . . . . . . . . . . . 16  |-  ( ( 1..^ i )  u.  ( ZZ>= `  i )
)  =  ( (
ZZ>= `  i )  u.  ( 1..^ i ) )
9089difeq1i 3536 . . . . . . . . . . . . . . 15  |-  ( ( ( 1..^ i )  u.  ( ZZ>= `  i
) )  \  (
1..^ i ) )  =  ( ( (
ZZ>= `  i )  u.  ( 1..^ i ) )  \  ( 1..^ i ) )
91 difun2 3838 . . . . . . . . . . . . . . 15  |-  ( ( ( ZZ>= `  i )  u.  ( 1..^ i ) )  \  ( 1..^ i ) )  =  ( ( ZZ>= `  i
)  \  ( 1..^ i ) )
9290, 91eqtri 2493 . . . . . . . . . . . . . 14  |-  ( ( ( 1..^ i )  u.  ( ZZ>= `  i
) )  \  (
1..^ i ) )  =  ( ( ZZ>= `  i )  \  (
1..^ i ) )
9388, 92syl6eq 2521 . . . . . . . . . . . . 13  |-  ( i  e.  NN  ->  ( NN  \  ( 1..^ i ) )  =  ( ( ZZ>= `  i )  \  ( 1..^ i ) ) )
94 difss 3549 . . . . . . . . . . . . 13  |-  ( (
ZZ>= `  i )  \ 
( 1..^ i ) )  C_  ( ZZ>= `  i )
9593, 94syl6eqss 3468 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  ( NN  \  ( 1..^ i ) )  C_  ( ZZ>=
`  i ) )
96 ssralv 3479 . . . . . . . . . . . 12  |-  ( ( NN  \  ( 1..^ i ) )  C_  ( ZZ>= `  i )  ->  ( A. k  e.  ( ZZ>= `  i )  -.  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  A. k  e.  ( NN  \  (
1..^ i ) )  -.  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) )  =  c ) )
9795, 96syl 17 . . . . . . . . . . 11  |-  ( i  e.  NN  ->  ( A. k  e.  ( ZZ>=
`  i )  -.  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  A. k  e.  ( NN  \  (
1..^ i ) )  -.  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) )  =  c ) )
98 impexp 453 . . . . . . . . . . . . . . 15  |-  ( ( ( k  e.  NN  /\ 
-.  k  e.  ( 1..^ i ) )  ->  -.  ( ( 1st `  ( G `  k ) )  oF  /  ( ( 1 ... N )  X.  { k } ) )  =  c )  <->  ( k  e.  NN  ->  ( -.  k  e.  ( 1..^ i )  ->  -.  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c ) ) )
99 eldif 3400 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( NN  \ 
( 1..^ i ) )  <->  ( k  e.  NN  /\  -.  k  e.  ( 1..^ i ) ) )
10099imbi1i 332 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  ( NN 
\  ( 1..^ i ) )  ->  -.  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )  <->  ( (
k  e.  NN  /\  -.  k  e.  (
1..^ i ) )  ->  -.  ( ( 1st `  ( G `  k ) )  oF  /  ( ( 1 ... N )  X.  { k } ) )  =  c ) )
101 con34b 299 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  k  e.  ( 1..^ i ) )  <->  ( -.  k  e.  ( 1..^ i )  ->  -.  ( ( 1st `  ( G `  k ) )  oF  /  ( ( 1 ... N )  X.  { k } ) )  =  c ) )
102101imbi2i 319 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN  ->  ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  k  e.  ( 1..^ i ) ) )  <->  ( k  e.  NN  ->  ( -.  k  e.  ( 1..^ i )  ->  -.  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c ) ) )
10398, 100, 1023bitr4i 285 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( NN 
\  ( 1..^ i ) )  ->  -.  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )  <->  ( k  e.  NN  ->  ( (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  k  e.  ( 1..^ i ) ) ) )
104103albii 1699 . . . . . . . . . . . . 13  |-  ( A. k ( k  e.  ( NN  \  (
1..^ i ) )  ->  -.  ( ( 1st `  ( G `  k ) )  oF  /  ( ( 1 ... N )  X.  { k } ) )  =  c )  <->  A. k ( k  e.  NN  ->  (
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  k  e.  ( 1..^ i ) ) ) )
105 df-ral 2761 . . . . . . . . . . . . 13  |-  ( A. k  e.  ( NN  \  ( 1..^ i ) )  -.  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  =  c  <->  A. k ( k  e.  ( NN  \ 
( 1..^ i ) )  ->  -.  (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c ) )
106 vex 3034 . . . . . . . . . . . . . . . 16  |-  c  e. 
_V
10755mptiniseg 5336 . . . . . . . . . . . . . . . 16  |-  ( c  e.  _V  ->  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " {
c } )  =  { k  e.  NN  |  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) )  =  c } )
108106, 107ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  =  {
k  e.  NN  | 
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c }
109108sseq1i 3442 . . . . . . . . . . . . . 14  |-  ( ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " {
c } )  C_  ( 1..^ i )  <->  { k  e.  NN  |  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  =  c }  C_  (
1..^ i ) )
110 rabss 3492 . . . . . . . . . . . . . 14  |-  ( { k  e.  NN  | 
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c }  C_  ( 1..^ i )  <->  A. k  e.  NN  ( ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  =  c  ->  k  e.  ( 1..^ i ) ) )
111 df-ral 2761 . . . . . . . . . . . . . 14  |-  ( A. k  e.  NN  (
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  k  e.  ( 1..^ i ) )  <->  A. k ( k  e.  NN  ->  (
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  k  e.  ( 1..^ i ) ) ) )
112109, 110, 1113bitri 279 . . . . . . . . . . . . 13  |-  ( ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " {
c } )  C_  ( 1..^ i )  <->  A. k
( k  e.  NN  ->  ( ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) )  =  c  -> 
k  e.  ( 1..^ i ) ) ) )
113104, 105, 1123bitr4i 285 . . . . . . . . . . . 12  |-  ( A. k  e.  ( NN  \  ( 1..^ i ) )  -.  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  =  c  <->  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  C_  (
1..^ i ) )
114 fzofi 12225 . . . . . . . . . . . . 13  |-  ( 1..^ i )  e.  Fin
115 ssfi 7810 . . . . . . . . . . . . 13  |-  ( ( ( 1..^ i )  e.  Fin  /\  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " {
c } )  C_  ( 1..^ i ) )  ->  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin )
116114, 115mpan 684 . . . . . . . . . . . 12  |-  ( ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " {
c } )  C_  ( 1..^ i )  -> 
( `' ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" { c } )  e.  Fin )
117113, 116sylbi 200 . . . . . . . . . . 11  |-  ( A. k  e.  ( NN  \  ( 1..^ i ) )  -.  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  =  c  ->  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin )
11897, 117syl6 33 . . . . . . . . . 10  |-  ( i  e.  NN  ->  ( A. k  e.  ( ZZ>=
`  i )  -.  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " {
c } )  e. 
Fin ) )
119118rexlimiv 2867 . . . . . . . . 9  |-  ( E. i  e.  NN  A. k  e.  ( ZZ>= `  i )  -.  (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " {
c } )  e. 
Fin )
120119ralimi 2796 . . . . . . . 8  |-  ( A. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) E. i  e.  NN  A. k  e.  ( ZZ>= `  i )  -.  (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  A. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin )
12182, 120sylbir 218 . . . . . . 7  |-  ( -. 
E. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  A. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin )
122 iunfi 7880 . . . . . . . 8  |-  ( ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  e.  Fin  /\ 
A. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin )  ->  U_ c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin )
123122ex 441 . . . . . . 7  |-  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  e.  Fin  ->  ( A. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin  ->  U_ c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin ) )
124121, 123syl5 32 . . . . . 6  |-  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  e.  Fin  ->  ( -.  E. c  e. 
ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  U_ c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) ( `' ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " { c } )  e.  Fin ) )
12575, 124mt3i 131 . . . . 5  |-  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  e.  Fin  ->  E. c  e.  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c )
126 ssrexv 3480 . . . . 5  |-  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  C_  I  ->  ( E. c  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  E. c  e.  I  A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c ) )
12758, 125, 126syl2im 38 . . . 4  |-  ( ph  ->  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )  e.  Fin  ->  E. c  e.  I  A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c ) )
128 unitssre 11805 . . . . . . . . . . . 12  |-  ( 0 [,] 1 )  C_  RR
129 elmapi 7511 . . . . . . . . . . . . . 14  |-  ( c  e.  ( ( 0 [,] 1 )  ^m  ( 1 ... N
) )  ->  c : ( 1 ... N ) --> ( 0 [,] 1 ) )
130129, 48eleq2s 2567 . . . . . . . . . . . . 13  |-  ( c  e.  I  ->  c : ( 1 ... N ) --> ( 0 [,] 1 ) )
131130ffvelrnda 6037 . . . . . . . . . . . 12  |-  ( ( c  e.  I  /\  m  e.  ( 1 ... N ) )  ->  ( c `  m )  e.  ( 0 [,] 1 ) )
132128, 131sseldi 3416 . . . . . . . . . . 11  |-  ( ( c  e.  I  /\  m  e.  ( 1 ... N ) )  ->  ( c `  m )  e.  RR )
133 nnrp 11334 . . . . . . . . . . . 12  |-  ( i  e.  NN  ->  i  e.  RR+ )
134133rpreccld 11374 . . . . . . . . . . 11  |-  ( i  e.  NN  ->  (
1  /  i )  e.  RR+ )
135 eqid 2471 . . . . . . . . . . . . 13  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
136135rexmet 21887 . . . . . . . . . . . 12  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  e.  ( *Met `  RR )
137 blcntr 21506 . . . . . . . . . . . 12  |-  ( ( ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )  e.  ( *Met `  RR )  /\  (
c `  m )  e.  RR  /\  ( 1  /  i )  e.  RR+ )  ->  ( c `
 m )  e.  ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) ) )
138136, 137mp3an1 1377 . . . . . . . . . . 11  |-  ( ( ( c `  m
)  e.  RR  /\  ( 1  /  i
)  e.  RR+ )  ->  ( c `  m
)  e.  ( ( c `  m ) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
139132, 134, 138syl2an 485 . . . . . . . . . 10  |-  ( ( ( c  e.  I  /\  m  e.  (
1 ... N ) )  /\  i  e.  NN )  ->  ( c `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
140139an32s 821 . . . . . . . . 9  |-  ( ( ( c  e.  I  /\  i  e.  NN )  /\  m  e.  ( 1 ... N ) )  ->  ( c `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
141 fveq1 5878 . . . . . . . . . 10  |-  ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  (
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  =  ( c `  m
) )
142141eleq1d 2533 . . . . . . . . 9  |-  ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  (
( ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) `  m )  e.  ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  <->  ( c `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) ) )
143140, 142syl5ibrcom 230 . . . . . . . 8  |-  ( ( ( c  e.  I  /\  i  e.  NN )  /\  m  e.  ( 1 ... N ) )  ->  ( (
( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  (
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) ) ) )
144143ralrimdva 2812 . . . . . . 7  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  ( ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) )  =  c  ->  A. m  e.  (
1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) ) ) )
145144reximdv 2857 . . . . . 6  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  ( E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  E. k  e.  ( ZZ>= `  i ) A. m  e.  (
1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) ) ) )
146145ralimdva 2805 . . . . 5  |-  ( c  e.  I  ->  ( A. i  e.  NN  E. k  e.  ( ZZ>= `  i ) ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) )  =  c  ->  A. i  e.  NN  E. k  e.  ( ZZ>= `  i ) A. m  e.  (
1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) ) ) )
147146reximia 2850 . . . 4  |-  ( E. c  e.  I  A. i  e.  NN  E. k  e.  ( ZZ>= `  i )
( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) )  =  c  ->  E. c  e.  I  A. i  e.  NN  E. k  e.  ( ZZ>= `  i ) A. m  e.  (
1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) ) )
148127, 147syl6 33 . . 3  |-  ( ph  ->  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )  e.  Fin  ->  E. c  e.  I  A. i  e.  NN  E. k  e.  ( ZZ>= `  i ) A. m  e.  (
1 ... N ) ( ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) `
 m )  e.  ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) ) ) )
149 poimir.r . . . . . . . 8  |-  R  =  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )
15051, 50ixpconst 7550 . . . . . . . . 9  |-  X_ n  e.  ( 1 ... N
) ( 0 [,] 1 )  =  ( ( 0 [,] 1
)  ^m  ( 1 ... N ) )
15148, 150eqtr4i 2496 . . . . . . . 8  |-  I  = 
X_ n  e.  ( 1 ... N ) ( 0 [,] 1
)
152149, 151oveq12i 6320 . . . . . . 7  |-  ( Rt  I )  =  ( (
Xt_ `  ( (
1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) )t  X_ n  e.  ( 1 ... N ) ( 0 [,] 1 ) )
153 fzfid 12224 . . . . . . . . 9  |-  ( T. 
->  ( 1 ... N
)  e.  Fin )
154 retop 21860 . . . . . . . . . . 11  |-  ( topGen ` 
ran  (,) )  e.  Top
155154fconst6 5786 . . . . . . . . . 10  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Top
156155a1i 11 . . . . . . . . 9  |-  ( T. 
->  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) --> Top )
15750a1i 11 . . . . . . . . 9  |-  ( ( T.  /\  n  e.  ( 1 ... N
) )  ->  (
0 [,] 1 )  e.  _V )
158153, 156, 157ptrest 32003 . . . . . . . 8  |-  ( T. 
->  ( ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) )t  X_ n  e.  ( 1 ... N
) ( 0 [,] 1 ) )  =  ( Xt_ `  (
n  e.  ( 1 ... N )  |->  ( ( ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) `  n )t  ( 0 [,] 1 ) ) ) ) )
159158trud 1461 . . . . . . 7  |-  ( (
Xt_ `  ( (
1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) )t  X_ n  e.  ( 1 ... N ) ( 0 [,] 1 ) )  =  ( Xt_ `  ( n  e.  ( 1 ... N ) 
|->  ( ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )t  ( 0 [,] 1 ) ) ) )
160 fvex 5889 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  e.  _V
161160fvconst2 6136 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)  =  ( topGen ` 
ran  (,) ) )
162161oveq1d 6323 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... N )  ->  (
( ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) `  n )t  ( 0 [,] 1 ) )  =  ( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) )
163162mpteq2ia 4478 . . . . . . . . 9  |-  ( n  e.  ( 1 ... N )  |->  ( ( ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)t  ( 0 [,] 1
) ) )  =  ( n  e.  ( 1 ... N ) 
|->  ( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) )
164 fconstmpt 4883 . . . . . . . . 9  |-  ( ( 1 ... N )  X.  { ( (
topGen `  ran  (,) )t  (
0 [,] 1 ) ) } )  =  ( n  e.  ( 1 ... N ) 
|->  ( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) )
165163, 164eqtr4i 2496 . . . . . . . 8  |-  ( n  e.  ( 1 ... N )  |->  ( ( ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  n
)t  ( 0 [,] 1
) ) )  =  ( ( 1 ... N )  X.  {
( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) } )
166165fveq2i 5882 . . . . . . 7  |-  ( Xt_ `  ( n  e.  ( 1 ... N ) 
|->  ( ( ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) `
 n )t  ( 0 [,] 1 ) ) ) )  =  (
Xt_ `  ( (
1 ... N )  X. 
{ ( ( topGen ` 
ran  (,) )t  ( 0 [,] 1 ) ) } ) )
167152, 159, 1663eqtri 2497 . . . . . 6  |-  ( Rt  I )  =  ( Xt_ `  ( ( 1 ... N )  X.  {
( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) } ) )
168 fzfi 12223 . . . . . . 7  |-  ( 1 ... N )  e. 
Fin
169 dfii2 21992 . . . . . . . . 9  |-  II  =  ( ( topGen `  ran  (,) )t  ( 0 [,] 1
) )
170 iicmp 21996 . . . . . . . . 9  |-  II  e.  Comp
171169, 170eqeltrri 2546 . . . . . . . 8  |-  ( (
topGen `  ran  (,) )t  (
0 [,] 1 ) )  e.  Comp
172171fconst6 5786 . . . . . . 7  |-  ( ( 1 ... N )  X.  { ( (
topGen `  ran  (,) )t  (
0 [,] 1 ) ) } ) : ( 1 ... N
) --> Comp
173 ptcmpfi 20905 . . . . . . 7  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( ( 1 ... N )  X.  {
( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) } ) : ( 1 ... N ) --> Comp )  ->  ( Xt_ `  (
( 1 ... N
)  X.  { ( ( topGen `  ran  (,) )t  (
0 [,] 1 ) ) } ) )  e.  Comp )
174168, 172, 173mp2an 686 . . . . . 6  |-  ( Xt_ `  ( ( 1 ... N )  X.  {
( ( topGen `  ran  (,) )t  ( 0 [,] 1
) ) } ) )  e.  Comp
175167, 174eqeltri 2545 . . . . 5  |-  ( Rt  I )  e.  Comp
176 rehaus 21895 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  e.  Haus
177176fconst6 5786 . . . . . . . . . . 11  |-  ( ( 1 ... N )  X.  { ( topGen ` 
ran  (,) ) } ) : ( 1 ... N ) --> Haus
178 pthaus 20730 . . . . . . . . . . 11  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) -->
Haus )  ->  ( Xt_ `  ( ( 1 ... N )  X. 
{ ( topGen `  ran  (,) ) } ) )  e.  Haus )
179168, 177, 178mp2an 686 . . . . . . . . . 10  |-  ( Xt_ `  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) )  e. 
Haus
180149, 179eqeltri 2545 . . . . . . . . 9  |-  R  e. 
Haus
181 haustop 20424 . . . . . . . . 9  |-  ( R  e.  Haus  ->  R  e. 
Top )
182180, 181ax-mp 5 . . . . . . . 8  |-  R  e. 
Top
183 reex 9648 . . . . . . . . . 10  |-  RR  e.  _V
184 mapss 7532 . . . . . . . . . 10  |-  ( ( RR  e.  _V  /\  ( 0 [,] 1
)  C_  RR )  ->  ( ( 0 [,] 1 )  ^m  (
1 ... N ) ) 
C_  ( RR  ^m  ( 1 ... N
) ) )
185183, 128, 184mp2an 686 . . . . . . . . 9  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  C_  ( RR  ^m  (
1 ... N ) )
18648, 185eqsstri 3448 . . . . . . . 8  |-  I  C_  ( RR  ^m  (
1 ... N ) )
187 uniretop 21861 . . . . . . . . . . 11  |-  RR  =  U. ( topGen `  ran  (,) )
188149, 187ptuniconst 20690 . . . . . . . . . 10  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( topGen `  ran  (,) )  e.  Top )  ->  ( RR  ^m  ( 1 ... N ) )  = 
U. R )
189168, 154, 188mp2an 686 . . . . . . . . 9  |-  ( RR 
^m  ( 1 ... N ) )  = 
U. R
190189restuni 20255 . . . . . . . 8  |-  ( ( R  e.  Top  /\  I  C_  ( RR  ^m  ( 1 ... N
) ) )  ->  I  =  U. ( Rt  I ) )
191182, 186, 190mp2an 686 . . . . . . 7  |-  I  = 
U. ( Rt  I )
192191bwth 20502 . . . . . 6  |-  ( ( ( Rt  I )  e.  Comp  /\ 
ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  C_  I  /\  -.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )  e.  Fin )  ->  E. c  e.  I 
c  e.  ( (
limPt `  ( Rt  I ) ) `  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ) )
1931923expia 1233 . . . . 5  |-  ( ( ( Rt  I )  e.  Comp  /\ 
ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  C_  I
)  ->  ( -.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  e.  Fin  ->  E. c  e.  I  c  e.  ( ( limPt `  ( Rt  I ) ) `  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ) ) )
194175, 58, 193sylancr 676 . . . 4  |-  ( ph  ->  ( -.  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  e.  Fin  ->  E. c  e.  I  c  e.  ( ( limPt `  ( Rt  I ) ) `  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) ) ) )
195 cmptop 20487 . . . . . . . . 9  |-  ( ( Rt  I )  e.  Comp  -> 
( Rt  I )  e.  Top )
196175, 195ax-mp 5 . . . . . . . 8  |-  ( Rt  I )  e.  Top
197191islp3 20239 . . . . . . . 8  |-  ( ( ( Rt  I )  e.  Top  /\ 
ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  C_  I  /\  c  e.  I
)  ->  ( c  e.  ( ( limPt `  ( Rt  I ) ) `  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )  <->  A. v  e.  ( Rt  I ) ( c  e.  v  ->  (
v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) ) )
198196, 197mp3an1 1377 . . . . . . 7  |-  ( ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  C_  I  /\  c  e.  I
)  ->  ( c  e.  ( ( limPt `  ( Rt  I ) ) `  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )  <->  A. v  e.  ( Rt  I ) ( c  e.  v  ->  (
v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) ) )
19958, 198sylan 479 . . . . . 6  |-  ( (
ph  /\  c  e.  I )  ->  (
c  e.  ( (
limPt `  ( Rt  I ) ) `  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )  <->  A. v  e.  ( Rt  I ) ( c  e.  v  ->  (
v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) ) )
200 fzfid 12224 . . . . . . . . . . . . 13  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  ( 1 ... N
)  e.  Fin )
201155a1i 11 . . . . . . . . . . . . 13  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  ( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) : ( 1 ... N ) --> Top )
202 nnrecre 10668 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  NN  ->  (
1  /  i )  e.  RR )
203202rexrd 9708 . . . . . . . . . . . . . . . 16  |-  ( i  e.  NN  ->  (
1  /  i )  e.  RR* )
204 eqid 2471 . . . . . . . . . . . . . . . . . . 19  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
205135, 204tgioo 21892 . . . . . . . . . . . . . . . . . 18  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
206205blopn 21593 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )  e.  ( *Met `  RR )  /\  (
c `  m )  e.  RR  /\  ( 1  /  i )  e. 
RR* )  ->  (
( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  e.  ( topGen ` 
ran  (,) ) )
207136, 206mp3an1 1377 . . . . . . . . . . . . . . . 16  |-  ( ( ( c `  m
)  e.  RR  /\  ( 1  /  i
)  e.  RR* )  ->  ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  e.  ( topGen `  ran  (,) )
)
208132, 203, 207syl2an 485 . . . . . . . . . . . . . . 15  |-  ( ( ( c  e.  I  /\  m  e.  (
1 ... N ) )  /\  i  e.  NN )  ->  ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  e.  ( topGen ` 
ran  (,) ) )
209208an32s 821 . . . . . . . . . . . . . 14  |-  ( ( ( c  e.  I  /\  i  e.  NN )  /\  m  e.  ( 1 ... N ) )  ->  ( (
c `  m )
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  e.  ( topGen ` 
ran  (,) ) )
210160fvconst2 6136 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  m
)  =  ( topGen ` 
ran  (,) ) )
211210adantl 473 . . . . . . . . . . . . . 14  |-  ( ( ( c  e.  I  /\  i  e.  NN )  /\  m  e.  ( 1 ... N ) )  ->  ( (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) `  m
)  =  ( topGen ` 
ran  (,) ) )
212209, 211eleqtrrd 2552 . . . . . . . . . . . . 13  |-  ( ( ( c  e.  I  /\  i  e.  NN )  /\  m  e.  ( 1 ... N ) )  ->  ( (
c `  m )
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  e.  ( ( ( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) `  m
) )
213 noel 3726 . . . . . . . . . . . . . . . 16  |-  -.  m  e.  (/)
214 difid 3747 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... N ) 
\  ( 1 ... N ) )  =  (/)
215214eleq2i 2541 . . . . . . . . . . . . . . . 16  |-  ( m  e.  ( ( 1 ... N )  \ 
( 1 ... N
) )  <->  m  e.  (/) )
216213, 215mtbir 306 . . . . . . . . . . . . . . 15  |-  -.  m  e.  ( ( 1 ... N )  \  (
1 ... N ) )
217216pm2.21i 136 . . . . . . . . . . . . . 14  |-  ( m  e.  ( ( 1 ... N )  \ 
( 1 ... N
) )  ->  (
( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  =  U. (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  m
) )
218217adantl 473 . . . . . . . . . . . . 13  |-  ( ( ( c  e.  I  /\  i  e.  NN )  /\  m  e.  ( ( 1 ... N
)  \  ( 1 ... N ) ) )  ->  ( (
c `  m )
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  =  U. (
( ( 1 ... N )  X.  {
( topGen `  ran  (,) ) } ) `  m
) )
219200, 201, 200, 212, 218ptopn 20675 . . . . . . . . . . . 12  |-  ( ( c  e.  I  /\  i  e.  NN )  -> 
X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  e.  ( Xt_ `  (
( 1 ... N
)  X.  { (
topGen `  ran  (,) ) } ) ) )
220219, 149syl6eleqr 2560 . . . . . . . . . . 11  |-  ( ( c  e.  I  /\  i  e.  NN )  -> 
X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  e.  R )
221 ovex 6336 . . . . . . . . . . . . 13  |-  ( ( 0 [,] 1 )  ^m  ( 1 ... N ) )  e. 
_V
22248, 221eqeltri 2545 . . . . . . . . . . . 12  |-  I  e. 
_V
223 elrestr 15405 . . . . . . . . . . . 12  |-  ( ( R  e.  Haus  /\  I  e.  _V  /\  X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  e.  R )  ->  ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I )  e.  ( Rt  I ) )
224180, 222, 223mp3an12 1380 . . . . . . . . . . 11  |-  ( X_ m  e.  ( 1 ... N ) ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  e.  R  -> 
( X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  i^i  I )  e.  ( Rt  I ) )
225220, 224syl 17 . . . . . . . . . 10  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I )  e.  ( Rt  I ) )
226 difss 3549 . . . . . . . . . . . . 13  |-  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) 
C_  ( ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" ( 1..^ i ) )
227 imassrn 5185 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  C_  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )
228226, 227sstri 3427 . . . . . . . . . . . 12  |-  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) 
C_  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )
229228, 58syl5ss 3429 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" ( 1..^ i ) )  \  {
c } )  C_  I )
230 haust1 20445 . . . . . . . . . . . . . 14  |-  ( R  e.  Haus  ->  R  e. 
Fre )
231180, 230ax-mp 5 . . . . . . . . . . . . 13  |-  R  e. 
Fre
232 restt1 20460 . . . . . . . . . . . . 13  |-  ( ( R  e.  Fre  /\  I  e.  _V )  ->  ( Rt  I )  e.  Fre )
233231, 222, 232mp2an 686 . . . . . . . . . . . 12  |-  ( Rt  I )  e.  Fre
234 funmpt 5625 . . . . . . . . . . . . . 14  |-  Fun  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )
235 imafi 7885 . . . . . . . . . . . . . 14  |-  ( ( Fun  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  /\  (
1..^ i )  e. 
Fin )  ->  (
( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  e. 
Fin )
236234, 114, 235mp2an 686 . . . . . . . . . . . . 13  |-  ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  e. 
Fin
237 diffi 7821 . . . . . . . . . . . . 13  |-  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  e. 
Fin  ->  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } )  e.  Fin )
238236, 237ax-mp 5 . . . . . . . . . . . 12  |-  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } )  e.  Fin
239191t1ficld 20420 . . . . . . . . . . . 12  |-  ( ( ( Rt  I )  e.  Fre  /\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" ( 1..^ i ) )  \  {
c } )  C_  I  /\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } )  e.  Fin )  -> 
( ( ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" ( 1..^ i ) )  \  {
c } )  e.  ( Clsd `  ( Rt  I ) ) )
240233, 238, 239mp3an13 1381 . . . . . . . . . . 11  |-  ( ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) 
\  { c } )  C_  I  ->  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) 
\  { c } )  e.  ( Clsd `  ( Rt  I ) ) )
241229, 240syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) )
" ( 1..^ i ) )  \  {
c } )  e.  ( Clsd `  ( Rt  I ) ) )
242191difopn 20126 . . . . . . . . . 10  |-  ( ( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I )  e.  ( Rt  I )  /\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } )  e.  ( Clsd `  ( Rt  I ) ) )  ->  ( ( X_ m  e.  ( 1 ... N ) ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  e.  ( Rt  I ) )
243225, 241, 242syl2anr 486 . . . . . . . . 9  |-  ( (
ph  /\  ( c  e.  I  /\  i  e.  NN ) )  -> 
( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  e.  ( Rt  I ) )
244243anassrs 660 . . . . . . . 8  |-  ( ( ( ph  /\  c  e.  I )  /\  i  e.  NN )  ->  (
( X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  i^i  I )  \  (
( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) 
\  { c } ) )  e.  ( Rt  I ) )
245 eleq2 2538 . . . . . . . . . . 11  |-  ( v  =  ( ( X_ m  e.  ( 1 ... N ) ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  ->  ( c  e.  v  <->  c  e.  ( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) ) ) )
246 ineq1 3618 . . . . . . . . . . . 12  |-  ( v  =  ( ( X_ m  e.  ( 1 ... N ) ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  ->  ( v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) 
\  { c } ) )  =  ( ( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) ) )
247246neeq1d 2702 . . . . . . . . . . 11  |-  ( v  =  ( ( X_ m  e.  ( 1 ... N ) ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  ->  ( (
v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) 
<->  ( ( ( X_ m  e.  ( 1 ... N ) ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) )
248245, 247imbi12d 327 . . . . . . . . . 10  |-  ( v  =  ( ( X_ m  e.  ( 1 ... N ) ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  ->  ( (
c  e.  v  -> 
( v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) )  <->  ( c  e.  ( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  ->  ( (
( X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  i^i  I )  \  (
( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) 
\  { c } ) )  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) ) )
249248rspcva 3134 . . . . . . . . 9  |-  ( ( ( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  e.  ( Rt  I )  /\  A. v  e.  ( Rt  I ) ( c  e.  v  ->  (
v  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) )  ->  (
c  e.  ( (
X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  i^i  I )  \  (
( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) 
\  { c } ) )  ->  (
( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  =/=  (/) ) )
250 ffn 5739 . . . . . . . . . . . . . . . 16  |-  ( c : ( 1 ... N ) --> ( 0 [,] 1 )  -> 
c  Fn  ( 1 ... N ) )
251130, 250syl 17 . . . . . . . . . . . . . . 15  |-  ( c  e.  I  ->  c  Fn  ( 1 ... N
) )
252251adantr 472 . . . . . . . . . . . . . 14  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  c  Fn  ( 1 ... N ) )
253140ralrimiva 2809 . . . . . . . . . . . . . 14  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  A. m  e.  ( 1 ... N ) ( c `  m
)  e.  ( ( c `  m ) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
254106elixp 7547 . . . . . . . . . . . . . 14  |-  ( c  e.  X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  <->  ( c  Fn  ( 1 ... N
)  /\  A. m  e.  ( 1 ... N
) ( c `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) ) )
255252, 253, 254sylanbrc 677 . . . . . . . . . . . . 13  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  c  e.  X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
256 simpl 464 . . . . . . . . . . . . 13  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  c  e.  I )
257255, 256elind 3609 . . . . . . . . . . . 12  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  c  e.  ( X_ m  e.  ( 1 ... N ) ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) )
258 neldifsnd 4091 . . . . . . . . . . . 12  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  -.  c  e.  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) 
\  { c } ) )
259257, 258eldifd 3401 . . . . . . . . . . 11  |-  ( ( c  e.  I  /\  i  e.  NN )  ->  c  e.  ( (
X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  i^i  I )  \  (
( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) 
\  { c } ) ) )
260259adantll 728 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  e.  I )  /\  i  e.  NN )  ->  c  e.  ( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) ) )
261 simplr 770 . . . . . . . . . . . . . . . . 17  |-  ( ( ( j  Fn  (
1 ... N )  /\  A. m  e.  ( 1 ... N ) ( j `  m )  e.  ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )  /\  j  e.  I )  ->  A. m  e.  ( 1 ... N
) ( j `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )
262261anim1i 578 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( j  Fn  ( 1 ... N
)  /\  A. m  e.  ( 1 ... N
) ( j `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )  /\  j  e.  I )  /\  -.  j  e.  ( (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) ) )  ->  ( A. m  e.  ( 1 ... N
) ( j `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  /\  -.  j  e.  ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) ) )
263 simpl 464 . . . . . . . . . . . . . . . 16  |-  ( ( j  e.  ran  (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  /\  -.  j  e.  { c } )  ->  j  e.  ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) )
264262, 263anim12i 576 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( j  Fn  ( 1 ... N )  /\  A. m  e.  ( 1 ... N ) ( j `  m )  e.  ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )  /\  j  e.  I )  /\  -.  j  e.  ( (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) ) )  /\  ( j  e. 
ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) )  /\  -.  j  e.  { c } ) )  -> 
( ( A. m  e.  ( 1 ... N
) ( j `  m )  e.  ( ( c `  m
) ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  /\  -.  j  e.  ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) )  /\  j  e. 
ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) ) )
265 elin 3608 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( ( (
X_ m  e.  ( 1 ... N ) ( ( c `  m ) ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) ( 1  / 
i ) )  i^i  I )  \  (
( ( k  e.  NN  |->  ( ( 1st `  ( G `  k
) )  oF  /  ( ( 1 ... N )  X. 
{ k } ) ) ) " (
1..^ i ) ) 
\  { c } ) )  i^i  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) )  \  { c } ) )  <->  ( j  e.  ( ( X_ m  e.  ( 1 ... N
) ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) )  i^i  I ) 
\  ( ( ( k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) )  \  { c } ) )  /\  j  e.  ( ran  ( k  e.  NN  |->  ( ( 1st `  ( G `
 k ) )  oF  /  (
( 1 ... N
)  X.  { k } ) ) ) 
\  { c } ) ) )
266 andir 885 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( j  Fn  ( 1 ... N )  /\  A. m  e.  ( 1 ... N ) ( j `  m )  e.  ( ( c `
 m ) (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) ( 1  /  i ) ) )  /\  j  e.  I )  /\  -.  j  e.  ( (
k  e.  NN  |->  ( ( 1st `  ( G `  k )
)  oF  / 
( ( 1 ... N )  X.  {
k } ) ) ) " ( 1..^ i ) ) )  \/  ( ( ( j  Fn  ( 1 ... N )  /\  A. m  e.  ( 1 ... N ) ( j `  m )  e.